1  /-
  2  Copyright (c) 2017 Johannes Hölzl. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Johannes Hölzl
  5  
  6  Borel (measurable) space -- the smallest σ-algebra generated by open sets
  7  
  8  It would be nice to encode this in the topological space type class, i.e. each topological space
  9  carries a measurable space, the Borel space. This would be similar how each uniform space carries a
 10  topological space. The idea is to allow definitional equality for product instances.
 11  We would like to have definitional equality for
 12  
 13    borel t₁ × borel t₂ = borel (t₁ × t₂)
 14  
 15  Unfortunately, this only holds if t₁ and t₂ are second-countable topologies.
 16  -/
 17  import measure_theory.measurable_space topology.instances.ennreal analysis.normed_space.basic
src         └─────────────────────────────┘ └────────────────────────┘ └─────────────────────────┘
 18  noncomputable theory
 19  
 20  open classical set lattice real
 21  open_locale classical
 22  
 23  universes u v w x y
 24  variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} {ι : Sort y} {s t u : set α}
id                                                                                       └─┘
src                                                                                      └─┘
typ                                                                                      └─┘
 25  
 26  open measurable_space topological_space
 27  
 28  @[instance, priority 900] def borel (α : Type u) [topological_space α] : measurable_space α :=
id                                                     └───────────────┘     └──────────────┘ 
src                                                    └───────────────┘      └──────────────┘
typ                                                    └───────────────┘     └──────────────┘ 
doc                                                    └───────────────┘
 29  generate_from {s : set α | is_open s}
id   └───────────┘     └─┘    └─────┘ 
src  └───────────┘     └─┘     └─────┘
typ  └───────────┘     └─┘    └─────┘ 
doc  └───────────┘              └─────┘
 30  
 31  lemma borel_eq_generate_from_of_subbasis {s : set (set α)}
id                                                 └─┘  └─┘ 
src                                                └─┘  └─┘
typ                                                └─┘  └─┘ 
 32    [t : topological_space α] [second_countable_topology α] (hs : t = generate_from s) :
id          └───────────────┘    └───────────────────────┘           └───────────┘ 
src         └───────────────┘     └───────────────────────┘             └───────────┘
typ         └───────────────┘    └───────────────────────┘           └───────────┘ 
doc         └───────────────┘     └───────────────────────┘              └───────────┘
 33    borel α = generate_from s :=
id     └───┘   └───────────┘ 
src    └───┘    └───────────┘
typ    └───┘   └───────────┘ 
doc              └───────────┘
 34  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
 35    (generate_from_le $ assume u (hu : t.is_open u),
id      └──────────────┘                 └──────┘ 
src     └──────────────┘                   └──────┘
typ     └──────────────┘                 └──────┘ 
 36      begin
st       └─────
 37        rw [hs] at hu,
id             └┘
src        └──┘  └─────┘
typ        └──┘└┘└─────┘
doc        └──┘  └─────┘
txt        └──┘  └─────┘
par        └──┘  └─────┘
pid          └┘  └────┘
st   ───────────┘└────┘└─
 38        induction hu,
id                   └┘
src        └────────┘
typ        └────────┘└┘
doc        └────────┘
txt        └────────┘
par        └────────┘
pid                 
st   ─────────────────┘└─
 39        case generate_open.basic : u hu
src        └───────────────────────────────
typ        └───────────────────────────────
doc        └───────────────────────────────
txt        └───────────────────────────────
par        └───────────────────────────────
pid            └──────────────────┘└─────┘
st   ──────────────────────────────────────
 40        { exact generate_measurable.basic u hu },
id                 └───────────────────────┘  └┘
src  ───────┘└────┘└───────────────────────┘   
typ  ───────┘└────┘└───────────────────────┘└┘
doc  ───────┘└────┘                            
txt  ───────┘└────┘                            
par  ───────┘└────┘                            
pid  ─────────────┘                            └┘
st   ──────┘└────────────────────────────────────┘└┘
 41        case generate_open.univ
src        └───────────────────────
typ        └───────────────────────
doc        └───────────────────────
txt        └───────────────────────
par        └───────────────────────
pid            └─────────────────┘
st   ──────────────────────────────
 42        { exact @is_measurable.univ α (generate_from s) },
id                  └────────────────┘   └───────────┘ 
src  ───────┘└────┘ └────────────────┘  └───────────┘ └┘
typ  ───────┘└────┘ └────────────────┘ └───────────┘└┘
doc  ───────┘└────┘                     └───────────┘ └┘
txt  ───────┘└────┘                                   └┘
par  ───────┘└────┘                                   └┘
pid  ─────┘└──────┘                                   └─┘
st   ──────┘└─────────────────────────────────────────────┘└┘
 43        case generate_open.inter : s₁ s₂ _ _ hs₁ hs₂
src        └────────────────────────────────────────────
typ        └────────────────────────────────────────────
doc        └────────────────────────────────────────────
txt        └────────────────────────────────────────────
par        └────────────────────────────────────────────
pid            └──────────────────┘└──────────────────┘
st   ───────────────────────────────────────────────────
 44        { exact @is_measurable.inter α (generate_from s) _ _ hs₁ hs₂ },
id                  └─────────────────┘   └───────────┘       └─┘ └─┘
src  ───────┘└────┘ └─────────────────┘  └───────────┘ └────┘      
typ  ───────┘└────┘ └─────────────────┘ └───────────┘└────┘└─┘└─┘
doc  ───────┘└────┘                      └───────────┘ └────┘      
txt  ───────┘└────┘                                    └────┘      
par  ───────┘└────┘                                    └────┘      
pid  ─────────────┘                                    └────┘      └┘
st   ──────┘└──────────────────────────────────────────────────────────┘└┘
 45        case generate_open.sUnion : f hf ih {
src        └─────────────────────────────────────
typ        └─────────────────────────────────────
doc        └─────────────────────────────────────
txt        └─────────────────────────────────────
par        └─────────────────────────────────────
pid            └───────────────────┘└────────┘└──
st   ──────────────────────────────────────────┘
 46          rcases is_open_sUnion_countable f (by rwa hs) with ⟨v, hv, vf, vu⟩,
id                  └──────────────────────┘          └┘
src  ───────┘└─────┘└──────────────────────┘    └──┘  └────────────────────┘└─
typ  ───────┘└─────┘└──────────────────────┘   └──┘└┘└────────────────────┘└─
doc  ───────┘└─────┘                            └──┘  └────────────────────┘└─
txt  ───────┘└─────┘                            └──┘  └────────────────────┘└─
par  ───────┘└─────┘                            └──┘  └────────────────────┘└─
pid  ──────────────┘                            └───┘  └───────────────────────
st   ────────────────────────────────────────────┘└─────┘└────────────────────┘└─
 47          rw ← vu,
id                └┘
src  ───────┘└───┘  └─
typ  ───────┘└───┘└┘└─
doc  ───────┘└───┘  └─
txt  ───────┘└───┘  └─
par  ───────┘└───┘  └─
pid  ────────────┘  └─
st   ──────────────┘└─
 48          exact @is_measurable.sUnion α (generate_from s) _ hv
id                  └──────────────────┘   └───────────┘     └┘
src  ───────┘└────┘ └──────────────────┘  └───────────┘ └──┘  
typ  ───────┘└────┘ └──────────────────┘ └───────────┘└──┘└┘
doc  ───────┘└────┘                       └───────────┘ └──┘  
txt  ───────┘└────┘                                     └──┘  
par  ───────┘└────┘                                     └──┘  
pid  ─────────────┘                                     └──┘  
st   ─────────────────────────────────────────────────────────────
 49            (λ x xv, ih _ (vf xv)) }
id                      └┘    └┘
src  ─────────┘  └─────┘  └─┘     └─┘└─
typ  ─────────┘  └─────┘└┘└─┘ └┘  └─┘└─
doc  ─────────┘  └─────┘  └─┘     └─┘└─
txt  ─────────┘  └─────┘  └─┘     └─┘└─
par  ─────────┘  └─────┘  └─┘     └─┘└─
pid  ─────────┘  └─────┘  └─┘     └──┘
st   ────────────────────────────────┘
 50      end)
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└─┘
 51    (generate_from_le $ assume u hu, generate_measurable.basic _ $
id      └──────────────┘           └┘  └───────────────────────┘
src     └──────────────┘                └───────────────────────┘
typ     └──────────────┘           └┘  └───────────────────────┘
 52      show t.is_open u, by rw [hs]; exact generate_open.basic _ hu)
id            └──────┘          └┘         └─────────────────┘   └┘
src            └──────┘       └──┘    └────┘└─────────────────┘└─┘
typ           └──────┘      └──┘└┘  └────┘└─────────────────┘└─┘└┘
doc                           └──┘    └────┘                   └─┘
txt                           └──┘    └────┘                   └─┘
par                           └──┘    └────┘                   └─┘
pid                             └┘                            └─┘
st                           └─────┘└──────────────────────────────┘
 53  
 54  lemma borel_eq_generate_Iio (α)
 55    [topological_space α] [second_countable_topology α]
id      └───────────────┘    └───────────────────────┘ 
src     └───────────────┘     └───────────────────────┘
typ     └───────────────┘    └───────────────────────┘ 
doc     └───────────────┘     └───────────────────────┘
 56    [linear_order α] [order_topology α] :
id      └──────────┘    └────────────┘ 
src     └──────────┘     └────────────┘
typ     └──────────┘    └────────────┘ 
doc                      └────────────┘
 57    borel α = generate_from (range Iio) :=
id     └───┘   └───────────┘  └───┘ └─┘
src    └───┘    └───────────┘  └───┘ └─┘
typ    └───┘   └───────────┘  └───┘ └─┘
doc              └───────────┘  └───┘ └─┘
 58  begin
st   └─────
 59    refine le_antisymm _ (generate_from_le _),
id            └─────────┘    └──────────────┘
src    └─────┘└─────────┘└─┘ └──────────────┘└─┘
typ    └─────┘└─────────┘└─┘ └──────────────┘└─┘
doc    └─────┘           └─┘                 └─┘
txt    └─────┘           └─┘                 └─┘
par    └─────┘           └─┘                 └─┘
pid                     └─┘                 └─┘
st   ──────────────────────────────────────────┘└─
 60    { rw borel_eq_generate_from_of_subbasis (order_topology.topology_eq_generate_intervals α),
id          └────────────────────────────────┘  └───────────────────────────────────────────┘ 
src      └─┘└────────────────────────────────┘ └───────────────────────────────────────────┘ 
typ      └─┘└────────────────────────────────┘ └───────────────────────────────────────────┘
doc      └─┘                                                                                 
txt      └─┘                                                                                 
par      └─┘                                                                                 
pid                                                                                         
st   ───┘└─────────────────────────────────────────────────────────────────────────────────────┘└─
 61      have H : ∀ a:α, is_measurable (measurable_space.generate_from (range Iio)) (Iio a) :=
id                      └───────────┘  └────────────────────────────┘  └───┘        └─┘
src      └───────┘ └─┘  └───────────┘ └────────────────────────────┘ └───┘   └─┘ └─┘ └────
typ      └───────┘ └─┘ └───────────┘ └────────────────────────────┘ └───┘   └─┘ └─┘ └────
doc      └───────┘ └─┘                └────────────────────────────┘ └───┘   └─┘ └─┘ └────
txt      └───────┘ └─┘                                                       └─┘     └────
par      └───────┘ └─┘                                                       └─┘     └────
pid      └────┘└─┘ └─┘                                                       └─┘     └───
st   ──────────────────────────────────────────────────────────────────────────────────────────
 62        λ a, generate_measurable.basic _ ⟨_, rfl⟩,
id              └───────────────────────┘       └─┘
src  ─────┘ └──┘└───────────────────────┘└─┘ └─┘└─┘
typ  ─────┘ └──┘└───────────────────────┘└─┘ └─┘└─┘
doc  ─────┘ └──┘                         └─┘ └─┘   
txt  ─────┘ └──┘                         └─┘ └─┘   
par  ─────┘ └──┘                         └─┘ └─┘   
pid  ─────┘ └──┘                         └─┘ └─┘   
st   ──────────────────────────────────────────────┘└─
 63      refine generate_from_le _, rintro _ ⟨a, rfl | rfl⟩; [skip, apply H],
id              └──────────────┘                             
src      └─────┘└──────────────┘└┘  └─────────────────────┘  └──┘  └────┘
typ      └─────┘└──────────────┘└┘  └─────────────────────┘  └──┘  └────┘
doc      └─────┘                └┘  └─────────────────────┘   └──┘  └────┘
txt      └─────┘                └┘  └─────────────────────┘   └──┘  └────┘
par      └─────┘                └┘  └─────────────────────┘   └──┘  └────┘
pid                            └┘        └───────────────┘              
st   ────────────────────────────┘└────────────────────────────────────────┘└─
 64      by_cases h : ∃ a', ∀ b, a < b ↔ a' ≤ b,
id                                     
src      └───────┘ └─┘└─┘ └┘     
typ      └───────┘ └─┘└─┘ └┘    
doc      └───────┘ └─┘ └─┘  └┘        
txt      └───────┘ └─┘ └─┘  └┘        
par      └───────┘ └─┘ └─┘  └┘        
pid               └─┘ └─┘  └┘        
st   ─────────────────────────────────────────┘└─
 65      { rcases h with ⟨a', ha'⟩,
id                
src        └─────┘ └─────────────┘
typ        └─────┘└─────────────┘
doc        └─────┘ └─────────────┘
txt        └─────┘ └─────────────┘
par        └─────┘ └─────────────┘
pid               └─────────────┘
st   ─────┘└─────────────────────┘└─
 66        rw (_ : Ioi a = -Iio a'), {exact (H _).compl _},
id                 └─┘   └─┘ └┘           
src        └─┘ └──┘└─┘ └─┘     └────┘  └─────────┘
typ        └─┘ └──┘└─┘└─┘└┘   └────┘ └─────────┘
doc        └─┘ └──┘└─┘   └─┘     └────┘  └─────────┘
txt        └─┘ └──┘              └────┘  └─────────┘
par        └─┘ └──┘              └────┘  └─────────┘
pid           └──┘                     └─────────┘
st   ─────────────────────────────┘└────────────────────┘└┘
 67        simp [set.ext_iff, ha'] },
id               └─────────┘  └─┘
src        └────┘└─────────┘└┘   └┘
typ        └────┘└─────────┘└┘└─┘└┘
doc        └────┘           └┘   └┘
txt        └────┘           └┘   └┘
par        └────┘           └┘   └┘
pid                       └┘   
st   ─────────────────────────────┘└┘
 68      { rcases is_open_Union_countable
id                └─────────────────────┘
src        └─────┘└─────────────────────┘
typ        └─────┘└─────────────────────┘
doc        └─────┘                       
txt        └─────┘                       
par        └─────┘                       
pid                                     
st   ─────────────────────────────────────
 69          (λ a' : {a' : α // a < a'}, {b | a'.1 < b})
id                                    
src  ───────┘  └────┘└───┘ └──┘    └─┘└──┘  └─┘  └──
typ  ───────┘  └────┘└───┘└──┘   └─┘└──┘  └─┘  └──
doc  ───────┘  └────┘ └───┘ └──┘    └─┘ └──┘  └─┘  └──
txt  ───────┘  └────┘ └───┘ └──┘    └─┘ └──┘  └─┘  └──
par  ───────┘  └────┘ └───┘ └──┘    └─┘ └──┘  └─┘  └──
pid  ───────┘  └────┘ └───┘ └──┘    └─┘ └──┘  └─┘  └──
st   ────────────────────────────────────────────────────
 70          (λ a', is_open_lt' _) with ⟨v, ⟨hv⟩, vu⟩,
id                  └─────────┘
src  ───────┘  └───┘└─────────┘└────────────────────┘
typ  ───────┘  └───┘└─────────┘└────────────────────┘
doc  ───────┘  └───┘           └────────────────────┘
txt  ───────┘  └───┘           └────────────────────┘
par  ───────┘  └───┘           └────────────────────┘
pid  ───────┘  └───┘           └────────────────────┘
st   ───────────────────────────────────────────────┘└─
 71        simp [set.ext_iff] at vu,
id               └─────────┘
src        └────┘└─────────┘└─────┘
typ        └────┘└─────────┘└─────┘
doc        └────┘           └─────┘
txt        └────┘           └─────┘
par        └────┘           └─────┘
pid                       └───┘
st   ─────────────────────────────┘└─
 72        have : Ioi a = ⋃ x : v, -Iio x.1.1,
id                └─┘           └─┘
src        └─────┘└─┘  └───┘  └─┘ └──┘
typ        └─────┘└─┘ └───┘ └─┘ └──┘
doc        └─────┘└─┘  └───┘  └─┘ └──┘
txt        └─────┘      └───┘       └──┘
par        └─────┘      └───┘       └──┘
pid        └───┘└┘      └───┘       └┘└┘
st   ───────────────────────────────────────┘└─
 73        { simp [set.ext_iff],
id                 └─────────┘
src          └────┘└─────────┘
typ          └────┘└─────────┘
doc          └────┘           
txt          └────┘           
par          └────┘           
pid                         
st   ───────┘└────────────────┘└─
 74          refine λ x, ⟨λ ax, _, λ ⟨a', ⟨h, av⟩, ax⟩, lt_of_lt_of_le h ax⟩,
id                                                └┘   └────────────┘
src          └─────┘ └──┘  └──────┘ └┘  └┘  └┘  └─┘  └─┘└────────────┘   
typ          └─────┘ └──┘  └──────┘ └┘  └┘ └┘  └─┘└┘└─┘└────────────┘   
doc          └─────┘ └──┘  └──────┘ └┘  └┘  └┘  └─┘  └─┘                 
txt          └─────┘ └──┘  └──────┘ └┘  └┘  └┘  └─┘  └─┘                 
par          └─────┘ └──┘  └──────┘ └┘  └┘  └┘  └─┘  └─┘                 
pid                 └──┘  └──────┘ └┘  └┘  └┘  └─┘  └─┘                 
st   ──────────────────────────────────────────────────────────────────────┘└─
 75          rcases (vu x).2 _ with ⟨a', h₁, h₂⟩,
id                   └┘ 
src          └─────┘    └─────────────────────┘
typ          └─────┘ └┘└─────────────────────┘
doc          └─────┘    └─────────────────────┘
txt          └─────┘    └─────────────────────┘
par          └─────┘    └─────────────────────┘
pid                    └─────────────────────┘
st   ──────────────────────────────────────────┘└─
 76          { exact ⟨a', h₁, le_of_lt h₂⟩ },
id                    └┘  └┘  └──────┘ └┘
src            └────┘   └┘  └┘└──────┘  └┘
typ            └────┘ └┘└┘└┘└┘└──────┘└┘└┘
doc            └────┘   └┘  └┘          └┘
txt            └────┘   └┘  └┘          └┘
par            └────┘   └┘  └┘          └┘
pid                    └┘  └┘          
st   ─────────┘└──────────────────────────┘└┘
 77          refine not_imp_comm.1 (λ h, _) h,
id                  └──────────┘            
src          └─────┘└──────────┘└─┘  └─────┘
typ          └─────┘└──────────┘└─┘  └─────┘
doc          └─────┘            └─┘  └─────┘
txt          └─────┘            └─┘  └─────┘
par          └─────┘            └─┘  └─────┘
pid                            └─┘  └─────┘
st   ───────────────────────────────────────┘└─
 78          exact ⟨x, λ b, ⟨λ ab, le_of_not_lt (λ h', h ⟨b, ab, h'⟩),
id                                └──────────┘        
src          └────┘  └┘ └──┘  └───┘└──────────┘  └───┘   └┘  └┘  └───
typ          └────┘ └┘ └──┘  └───┘└──────────┘  └───┘  └┘  └┘  └───
doc          └────┘  └┘ └──┘  └───┘              └───┘   └┘  └┘  └───
txt          └────┘  └┘ └──┘  └───┘              └───┘   └┘  └┘  └───
par          └────┘  └┘ └──┘  └───┘              └───┘   └┘  └┘  └───
pid                 └┘ └──┘  └───┘              └───┘   └┘  └┘  └───
st   ──────────────────────────────────────────────────────────────────
 79            lt_of_lt_of_le ax⟩⟩ },
id             └────────────┘ └┘
src  ─────────┘└────────────┘  └─┘
typ  ─────────┘└────────────┘└┘└─┘
doc  ─────────┘                └─┘
txt  ─────────┘                └─┘
par  ─────────┘                └─┘
pid  ─────────┘                └┘
st   ─────────────────────────────┘└┘
 80        rw this, resetI,
id            └──┘
src        └─┘      └────┘
typ        └─┘└──┘  └────┘
doc        └─┘      └────┘
txt        └─┘      └────┘
par        └─┘      └────┘
pid          
st   ────────────┘└─────────
 81        apply is_measurable.Union,
id               └─────────────────┘
src        └────┘└─────────────────┘
typ        └────┘└─────────────────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ──────────────────────────────┘└─
 82        exact λ _, (H _).compl _ } },
id                     
src        └────┘ └──┘  └──────────┘
typ        └────┘ └──┘ └──────────┘
doc        └────┘ └──┘  └──────────┘
txt        └────┘ └──┘  └──────────┘
par        └────┘ └──┘  └──────────┘
pid              └──┘  └─────────┘
st   ──────────────────────────────┘└──┘
 83    { simp, rintro _ a rfl,
src      └──┘  └────────────┘
typ      └──┘  └────────────┘
doc      └──┘  └────────────┘
txt      └──┘  └────────────┘
par      └──┘  └────────────┘
pid                  └──────┘
st   ───────┘└──────────────┘└─
 84      exact generate_measurable.basic _ is_open_Iio }
id             └───────────────────────┘   └─────────┘
src      └────┘└───────────────────────┘└─┘└─────────┘
typ      └────┘└───────────────────────┘└─┘└─────────┘
doc      └────┘                         └─┘           
txt      └────┘                         └─┘           
par      └────┘                         └─┘           
pid                                    └─┘           
st   ─────────────────────────────────────────────────┘└─
 85  end
st   ──┘
 86  
 87  lemma borel_eq_generate_Ioi (α)
 88    [topological_space α] [second_countable_topology α]
id      └───────────────┘    └───────────────────────┘ 
src     └───────────────┘     └───────────────────────┘
typ     └───────────────┘    └───────────────────────┘ 
doc     └───────────────┘     └───────────────────────┘
 89    [linear_order α] [order_topology α] :
id      └──────────┘    └────────────┘ 
src     └──────────┘     └────────────┘
typ     └──────────┘    └────────────┘ 
doc                      └────────────┘
 90    borel α = generate_from (range (λ a, {x | a < x})) :=
id     └───┘   └───────────┘  └───┘           
src    └───┘    └───────────┘  └───┘             
typ    └───┘   └───────────┘  └───┘           
doc              └───────────┘  └───┘
 91  begin
st   └─────
 92    refine le_antisymm _ (generate_from_le _),
id            └─────────┘    └──────────────┘
src    └─────┘└─────────┘└─┘ └──────────────┘└─┘
typ    └─────┘└─────────┘└─┘ └──────────────┘└─┘
doc    └─────┘           └─┘                 └─┘
txt    └─────┘           └─┘                 └─┘
par    └─────┘           └─┘                 └─┘
pid                     └─┘                 └─┘
st   ──────────────────────────────────────────┘└─
 93    { rw borel_eq_generate_from_of_subbasis (order_topology.topology_eq_generate_intervals α),
id          └────────────────────────────────┘  └───────────────────────────────────────────┘ 
src      └─┘└────────────────────────────────┘ └───────────────────────────────────────────┘ 
typ      └─┘└────────────────────────────────┘ └───────────────────────────────────────────┘
doc      └─┘                                                                                 
txt      └─┘                                                                                 
par      └─┘                                                                                 
pid                                                                                         
st   ───┘└─────────────────────────────────────────────────────────────────────────────────────┘└─
 94      have H : ∀ a:α, is_measurable (measurable_space.generate_from (range (λ a, {x | a < x}))) {x | a < x} :=
id                      └───────────┘  └────────────────────────────┘  └───┘                     
src      └───────┘ └─┘  └───────────┘ └────────────────────────────┘ └───┘  └──┘ └──┘  └───┘└──┘   └────
typ      └───────┘ └─┘ └───────────┘ └────────────────────────────┘ └───┘  └──┘ └──┘  └───┘└──┘   └────
doc      └───────┘ └─┘                └────────────────────────────┘ └───┘  └──┘ └──┘   └───┘ └──┘   └────
txt      └───────┘ └─┘                                                      └──┘ └──┘   └───┘ └──┘   └────
par      └───────┘ └─┘                                                      └──┘ └──┘   └───┘ └──┘   └────
pid      └────┘└─┘ └─┘                                                      └──┘ └──┘   └───┘ └──┘   └───
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────────────
 95        λ a, generate_measurable.basic _ ⟨_, rfl⟩,
id              └───────────────────────┘       └─┘
src  ─────┘ └──┘└───────────────────────┘└─┘ └─┘└─┘
typ  ─────┘ └──┘└───────────────────────┘└─┘ └─┘└─┘
doc  ─────┘ └──┘                         └─┘ └─┘   
txt  ─────┘ └──┘                         └─┘ └─┘   
par  ─────┘ └──┘                         └─┘ └─┘   
pid  ─────┘ └──┘                         └─┘ └─┘   
st   ──────────────────────────────────────────────┘└─
 96      refine generate_from_le _, rintro _ ⟨a, rfl | rfl⟩, {apply H},
id              └──────────────┘
src      └─────┘└──────────────┘└┘  └─────────────────────┘   └────┘
typ      └─────┘└──────────────┘└┘  └─────────────────────┘   └────┘
doc      └─────┘                └┘  └─────────────────────┘   └────┘
txt      └─────┘                └┘  └─────────────────────┘   └────┘
par      └─────┘                └┘  └─────────────────────┘   └────┘
pid                            └┘        └───────────────┘        
st   ────────────────────────────┘└───────────────────────┘└────────┘└┘
 97      by_cases h : ∃ a', ∀ b, b < a ↔ b ≤ a',
id                                     
src      └───────┘ └─┘└─┘ └┘     
typ      └───────┘ └─┘└─┘ └┘    
doc      └───────┘ └─┘ └─┘  └┘       
txt      └───────┘ └─┘ └─┘  └┘       
par      └───────┘ └─┘ └─┘  └┘       
pid               └─┘ └─┘  └┘       
st   ─────────────────────────────────────────┘└─
 98      { rcases h with ⟨a', ha'⟩,
id                
src        └─────┘ └─────────────┘
typ        └─────┘└─────────────┘
doc        └─────┘ └─────────────┘
txt        └─────┘ └─────────────┘
par        └─────┘ └─────────────┘
pid               └─────────────┘
st   ─────┘└─────────────────────┘└─
 99        rw (_ : Iio a = -Ioi a'), {exact (H _).compl _},
id                 └─┘   └─┘ └┘           
src        └─┘ └──┘└─┘ └─┘     └────┘  └─────────┘
typ        └─┘ └──┘└─┘└─┘└┘   └────┘ └─────────┘
doc        └─┘ └──┘└─┘   └─┘     └────┘  └─────────┘
txt        └─┘ └──┘              └────┘  └─────────┘
par        └─┘ └──┘              └────┘  └─────────┘
pid           └──┘                     └─────────┘
st   ─────────────────────────────┘└────────────────────┘└┘
100        simp [set.ext_iff, ha'] },
id               └─────────┘  └─┘
src        └────┘└─────────┘└┘   └┘
typ        └────┘└─────────┘└┘└─┘└┘
doc        └────┘           └┘   └┘
txt        └────┘           └┘   └┘
par        └────┘           └┘   └┘
pid                       └┘   
st   ─────────────────────────────┘└┘
101      { rcases is_open_Union_countable
id                └─────────────────────┘
src        └─────┘└─────────────────────┘
typ        └─────┘└─────────────────────┘
doc        └─────┘                       
txt        └─────┘                       
par        └─────┘                       
pid                                     
st   ─────────────────────────────────────
102          (λ a' : {a' : α // a' < a}, {b | b < a'.1})
id                                    
src  ───────┘  └────┘└───┘ └──┘    └─┘└──┘    └────
typ  ───────┘  └────┘└───┘└──┘   └─┘└──┘    └────
doc  ───────┘  └────┘ └───┘ └──┘    └─┘ └──┘    └────
txt  ───────┘  └────┘ └───┘ └──┘    └─┘ └──┘    └────
par  ───────┘  └────┘ └───┘ └──┘    └─┘ └──┘    └────
pid  ───────┘  └────┘ └───┘ └──┘    └─┘ └──┘    └────
st   ────────────────────────────────────────────────────
103          (λ a', is_open_gt' _) with ⟨v, ⟨hv⟩, vu⟩,
id                  └─────────┘
src  ───────┘  └───┘└─────────┘└────────────────────┘
typ  ───────┘  └───┘└─────────┘└────────────────────┘
doc  ───────┘  └───┘           └────────────────────┘
txt  ───────┘  └───┘           └────────────────────┘
par  ───────┘  └───┘           └────────────────────┘
pid  ───────┘  └───┘           └────────────────────┘
st   ───────────────────────────────────────────────┘└─
104        simp [set.ext_iff] at vu,
id               └─────────┘
src        └────┘└─────────┘└─────┘
typ        └────┘└─────────┘└─────┘
doc        └────┘           └─────┘
txt        └────┘           └─────┘
par        └────┘           └─────┘
pid                       └───┘
st   ─────────────────────────────┘
105        have : Iio a = ⋃ x : v, -Ioi x.1.1,
id                └─┘           └─┘
src        └─────┘└─┘  └───┘  └─┘ └──┘
typ        └─────┘└─┘ └───┘ └─┘ └──┘
doc        └─────┘└─┘  └───┘  └─┘ └──┘
txt        └─────┘      └───┘       └──┘
par        └─────┘      └───┘       └──┘
pid        └───┘└┘      └───┘       └┘└┘
st   └──────────────────────────────────────┘└─
106        { simp [set.ext_iff],
id                 └─────────┘
src          └────┘└─────────┘
typ          └────┘└─────────┘
doc          └────┘           
txt          └────┘           
par          └────┘           
pid                         
st   ───────┘└────────────────┘└─
107          refine λ x, ⟨λ ax, _, λ ⟨a', ⟨h, av⟩, ax⟩, lt_of_le_of_lt ax h⟩,
id                                                └┘   └────────────┘
src          └─────┘ └──┘  └──────┘ └┘  └┘  └┘  └─┘  └─┘└────────────┘   
typ          └─────┘ └──┘  └──────┘ └┘  └┘ └┘  └─┘└┘└─┘└────────────┘   
doc          └─────┘ └──┘  └──────┘ └┘  └┘  └┘  └─┘  └─┘                 
txt          └─────┘ └──┘  └──────┘ └┘  └┘  └┘  └─┘  └─┘                 
par          └─────┘ └──┘  └──────┘ └┘  └┘  └┘  └─┘  └─┘                 
pid                 └──┘  └──────┘ └┘  └┘  └┘  └─┘  └─┘                 
st   ──────────────────────────────────────────────────────────────────────┘└─
108          rcases (vu x).2 _ with ⟨a', h₁, h₂⟩,
id                   └┘ 
src          └─────┘    └─────────────────────┘
typ          └─────┘ └┘└─────────────────────┘
doc          └─────┘    └─────────────────────┘
txt          └─────┘    └─────────────────────┘
par          └─────┘    └─────────────────────┘
pid                    └─────────────────────┘
st   ──────────────────────────────────────────┘└─
109          { exact ⟨a', h₁, le_of_lt h₂⟩ },
id                    └┘  └┘  └──────┘ └┘
src            └────┘   └┘  └┘└──────┘  └┘
typ            └────┘ └┘└┘└┘└┘└──────┘└┘└┘
doc            └────┘   └┘  └┘          └┘
txt            └────┘   └┘  └┘          └┘
par            └────┘   └┘  └┘          └┘
pid                    └┘  └┘          
st   ─────────┘└──────────────────────────┘└┘
110          refine not_imp_comm.1 (λ h, _) h,
id                  └──────────┘            
src          └─────┘└──────────┘└─┘  └─────┘
typ          └─────┘└──────────┘└─┘  └─────┘
doc          └─────┘            └─┘  └─────┘
txt          └─────┘            └─┘  └─────┘
par          └─────┘            └─┘  └─────┘
pid                            └─┘  └─────┘
st   ───────────────────────────────────────┘└─
111          exact ⟨x, λ b, ⟨λ ab, le_of_not_lt (λ h', h ⟨b, ab, h'⟩),
id                                └──────────┘        
src          └────┘  └┘ └──┘  └───┘└──────────┘  └───┘   └┘  └┘  └───
typ          └────┘ └┘ └──┘  └───┘└──────────┘  └───┘  └┘  └┘  └───
doc          └────┘  └┘ └──┘  └───┘              └───┘   └┘  └┘  └───
txt          └────┘  └┘ └──┘  └───┘              └───┘   └┘  └┘  └───
par          └────┘  └┘ └──┘  └───┘              └───┘   └┘  └┘  └───
pid                 └┘ └──┘  └───┘              └───┘   └┘  └┘  └───
st   ──────────────────────────────────────────────────────────────────
112            λ h, lt_of_le_of_lt h ax⟩⟩ },
id                  └────────────┘   └┘
src  ─────────┘ └──┘└────────────┘   └─┘
typ  ─────────┘ └──┘└────────────┘ └┘└─┘
doc  ─────────┘ └──┘                 └─┘
txt  ─────────┘ └──┘                 └─┘
par  ─────────┘ └──┘                 └─┘
pid  ─────────┘ └──┘                 └┘
st   ────────────────────────────────────┘└┘
113        rw this, resetI,
id            └──┘
src        └─┘      └────┘
typ        └─┘└──┘  └────┘
doc        └─┘      └────┘
txt        └─┘      └────┘
par        └─┘      └────┘
pid          
st   ────────────┘└─────────
114        apply is_measurable.Union,
id               └─────────────────┘
src        └────┘└─────────────────┘
typ        └────┘└─────────────────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ──────────────────────────────┘└─
115        exact λ _, (H _).compl _ } },
id                     
src        └────┘ └──┘  └──────────┘
typ        └────┘ └──┘ └──────────┘
doc        └────┘ └──┘  └──────────┘
txt        └────┘ └──┘  └──────────┘
par        └────┘ └──┘  └──────────┘
pid              └──┘  └─────────┘
st   ──────────────────────────────┘└──┘
116    { simp, rintro _ a rfl,
src      └──┘  └────────────┘
typ      └──┘  └────────────┘
doc      └──┘  └────────────┘
txt      └──┘  └────────────┘
par      └──┘  └────────────┘
pid                  └──────┘
st   ───────┘└──────────────┘└─
117      exact generate_measurable.basic _ (is_open_lt' _) }
id             └───────────────────────┘    └─────────┘
src      └────┘└───────────────────────┘└─┘ └─────────┘└──┘
typ      └────┘└───────────────────────┘└─┘ └─────────┘└──┘
doc      └────┘                         └─┘            └──┘
txt      └────┘                         └─┘            └──┘
par      └────┘                         └─┘            └──┘
pid                                    └─┘            └─┘
st   ─────────────────────────────────────────────────────┘└─
118  end
st   ──┘
119  
120  lemma borel_comap {f : α → β} {t : topological_space β} :
id                                    └───────────────┘ 
src                                     └───────────────┘
typ                                   └───────────────┘ 
doc                                     └───────────────┘
121    @borel α (t.induced f) = (@borel β t).comap f :=
id      └───┘   └──────┘      └───┘   └───┘  
src     └───┘     └──────┘       └───┘     └───┘
typ     └───┘   └──────┘      └───┘   └───┘  
doc               └──────┘                  └───┘
122  calc @borel α (t.induced f) =
id         └───┘   └──────┘ 
src        └───┘     └──────┘
typ        └───┘   └──────┘ 
doc                  └──────┘
123      measurable_space.generate_from (preimage f '' {s | is_open s }) :
id       └────────────────────────────┘  └──────┘  └┘    └─────┘ 
src      └────────────────────────────┘  └──────┘   └┘     └─────┘
typ      └────────────────────────────┘  └──────┘  └┘    └─────┘ 
doc      └────────────────────────────┘  └──────┘           └─────┘
124        congr_arg measurable_space.generate_from $ set.ext $ assume s : set α,
id         └───────┘ └────────────────────────────┘   └─────┘              └─┘ 
src        └───────┘ └────────────────────────────┘   └─────┘              └─┘
typ        └───────┘ └────────────────────────────┘   └─────┘              └─┘ 
doc                  └────────────────────────────┘
125        show (t.induced f).is_open s ↔ s ∈ preimage f '' {s | is_open s},
id               └──────┘  └─────┘      └──────┘  └┘    └─────┘ 
src               └──────┘   └─────┘        └──────┘   └┘     └─────┘
typ              └──────┘  └─────┘      └──────┘  └┘    └─────┘ 
doc               └──────┘                    └──────┘           └─────┘
126          by simp [topological_space.induced, set.image, eq_comm]; refl
id                    └───────────────────────┘  └───────┘  └─────┘
src             └────┘└───────────────────────┘└┘└───────┘└┘└─────┘  └────
typ             └────┘└───────────────────────┘└┘└───────┘└┘└─────┘  └────
doc             └────┘└───────────────────────┘└┘         └┘         └────
txt             └────┘                         └┘         └┘         └────
par             └────┘                         └┘         └┘         └────
pid                                          └┘         └┘             
st             └───────────────────────────────────────────────────────────
127    ... = (@borel β t).comap f : comap_generate_from.symm
id             └───┘   └───┘     └─────────────────┘└───┘
src  ─┘        └───┘     └───┘      └─────────────────┘└───┘
typ  ─┘        └───┘   └───┘     └─────────────────┘└───┘
doc  ─┘                  └───┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
128  
129  section
130  variables [topological_space α]
id              └───────────────┘
src             └───────────────┘
typ             └───────────────┘
doc             └───────────────┘
131  
132  lemma is_measurable_of_is_open : is_open s → is_measurable s := generate_measurable.basic s
id                                    └─────┘    └───────────┘     └───────────────────────┘ 
src                                   └─────┘     └───────────┘      └───────────────────────┘
typ                                   └─────┘    └───────────┘     └───────────────────────┘ 
doc                                   └─────┘     └───────────┘
133  
134  lemma is_measurable_interior : is_measurable (interior s) :=
id                                  └───────────┘  └──────┘ 
src                                 └───────────┘  └──────┘
typ                                 └───────────┘  └──────┘ 
doc                                 └───────────┘  └──────┘
135  is_measurable_of_is_open is_open_interior
id   └──────────────────────┘ └──────────────┘
src  └──────────────────────┘ └──────────────┘
typ  └──────────────────────┘ └──────────────┘
136  
137  lemma is_measurable_ball [metric_space β] {x : β} {ε : ℝ} : is_measurable (metric.ball x ε) :=
id                             └──────────┘                   └───────────┘  └─────────┘  
src                            └──────────┘                     └───────────┘  └─────────┘
typ                            └──────────┘                   └───────────┘  └─────────┘  
doc                            └──────────┘                      └───────────┘  └─────────┘
138  is_measurable_of_is_open metric.is_open_ball
id   └──────────────────────┘ └─────────────────┘
src  └──────────────────────┘ └─────────────────┘
typ  └──────────────────────┘ └─────────────────┘
139  
140  lemma is_measurable_of_is_closed (h : is_closed s) : is_measurable s :=
id                                         └───────┘     └───────────┘ 
src                                        └───────┘      └───────────┘
typ                                        └───────┘     └───────────┘ 
doc                                        └───────┘      └───────────┘
141  is_measurable.compl_iff.1 $ is_measurable_of_is_open h
id   └─────────────────────┘    └──────────────────────┘ 
src  └─────────────────────┘    └──────────────────────┘
typ  └─────────────────────┘    └──────────────────────┘ 
142  
143  lemma is_measurable_singleton [t1_space α] {x : α} : is_measurable ({x} : set α) :=
id                                  └──────┘            └───────────┘      └─┘ 
src                                 └──────┘              └───────────┘       └─┘
typ                                 └──────┘            └───────────┘      └─┘ 
doc                                 └──────┘              └───────────┘
144  is_measurable_of_is_closed is_closed_singleton
id   └────────────────────────┘ └─────────────────┘
src  └────────────────────────┘ └─────────────────┘
typ  └────────────────────────┘ └─────────────────┘
145  
146  lemma is_measurable_closure : is_measurable (closure s) :=
id                                 └───────────┘  └─────┘ 
src                                └───────────┘  └─────┘
typ                                └───────────┘  └─────┘ 
doc                                └───────────┘  └─────┘
147  is_measurable_of_is_closed is_closed_closure
id   └────────────────────────┘ └───────────────┘
src  └────────────────────────┘ └───────────────┘
typ  └────────────────────────┘ └───────────────┘
148  
149  lemma measurable_of_continuous [topological_space β] {f : α → β} (h : continuous f) :
id                                   └───────────────┘                  └────────┘ 
src                                  └───────────────┘                     └────────┘
typ                                  └───────────────┘                  └────────┘ 
doc                                  └───────────────┘                     └────────┘
150    measurable f :=
id     └────────┘ 
src    └────────┘
typ    └────────┘ 
doc    └────────┘
151  measurable_generate_from $ assume t ht, is_measurable_of_is_open $ h t ht
id   └──────────────────────┘           └┘  └──────────────────────┘     └┘
src  └──────────────────────┘                └──────────────────────┘
typ  └──────────────────────┘           └┘  └──────────────────────┘     └┘
152  
153  lemma borel_prod_le [topological_space β] :
id                        └───────────────┘ 
src                       └───────────────┘
typ                       └───────────────┘ 
doc                       └───────────────┘
154    prod.measurable_space ≤ borel (α × β) :=
id     └───────────────────┘  └───┘    
src    └───────────────────┘  └───┘    
typ    └───────────────────┘  └───┘    
155  sup_le
id   └────┘
src  └────┘
typ  └────┘
156    (comap_le_iff_le_map.mpr $ measurable_of_continuous continuous_fst)
id      └─────────────────┘└──┘   └──────────────────────┘ └────────────┘
src     └─────────────────┘└──┘   └──────────────────────┘ └────────────┘
typ     └─────────────────┘└──┘   └──────────────────────┘ └────────────┘
157    (comap_le_iff_le_map.mpr $ measurable_of_continuous continuous_snd)
id      └─────────────────┘└──┘   └──────────────────────┘ └────────────┘
src     └─────────────────┘└──┘   └──────────────────────┘ └────────────┘
typ     └─────────────────┘└──┘   └──────────────────────┘ └────────────┘
158  
159  lemma borel_induced {α β} [t : topological_space β] (f : α → β) :
id                                  └───────────────┘           
src                                 └───────────────┘
typ                                 └───────────────┘           
doc                                 └───────────────┘
160    @borel α (t.induced f) = (borel β).comap f :=
id      └───┘   └──────┘     └───┘  └───┘  
src     └───┘     └──────┘      └───┘   └───┘
typ     └───┘   └──────┘     └───┘  └───┘  
doc               └──────┘               └───┘
161  comap_generate_from.symm
id   └─────────────────┘└───┘
src  └─────────────────┘└───┘
typ  └─────────────────┘└───┘
162  
163  lemma borel_eq_subtype (s : set α) : borel s = subtype.measurable_space :=
id                               └─┘     └───┘   └──────────────────────┘
src                              └─┘      └───┘    └──────────────────────┘
typ                              └─┘     └───┘   └──────────────────────┘
164  borel_induced coe
id   └───────────┘ └─┘
src  └───────────┘ └─┘
typ  └───────────┘ └─┘
165  
166  lemma borel_prod [second_countable_topology α] [topological_space β] [second_countable_topology β] :
id                     └───────────────────────┘    └───────────────┘    └───────────────────────┘ 
src                    └───────────────────────┘     └───────────────┘     └───────────────────────┘
typ                    └───────────────────────┘    └───────────────┘    └───────────────────────┘ 
doc                    └───────────────────────┘     └───────────────┘     └───────────────────────┘
167    prod.measurable_space = borel (α × β) :=
id     └───────────────────┘  └───┘    
src    └───────────────────┘  └───┘    
typ    └───────────────────┘  └───┘    
168  let ⟨a, ha₁, ha₂, ha₃, ha₄, ha₅⟩ := @is_open_generated_countable_inter α _ _ in
id   └─┘                                  └───────────────────────────────┘ 
src                                       └───────────────────────────────┘
typ  └─┘                                  └───────────────────────────────┘ 
169  let ⟨b, hb₁, hb₂, hb₃, hb₄, hb₅⟩ := @is_open_generated_countable_inter β _ _ in
id   └─┘                                  └───────────────────────────────┘ 
src                                       └───────────────────────────────┘
typ  └─┘                                  └───────────────────────────────┘ 
170  le_antisymm borel_prod_le begin
id   └─────────┘ └───────────┘
src  └─────────┘ └───────────┘
typ  └─────────┘ └───────────┘
st                             └─────
171      have : prod.topological_space = generate_from {g | ∃u∈a, ∃v∈b, g = set.prod u v},
id              └────────────────────┘  └───────────┘                 └──────┘
src      └─────┘└────────────────────┘└───────────┘└──┘└┘  └┘    └──────┘  
typ      └─────┘└────────────────────┘└───────────┘└──┘└┘ └┘   └──────┘  
doc      └─────┘                       └───────────┘ └──┘ └┘   └┘    └──────┘  
txt      └─────┘                                     └──┘ └┘   └┘              
par      └─────┘                                     └──┘ └┘   └┘              
pid      └───┘└┘                                     └──┘ └┘   └┘              
st   ───────────────────────────────────────────────────────────────────────────────────┘└─
172      { rw [ha₅, hb₅], exact prod_generate_from_generate_from_eq ha₄ hb₄ },
id             └─┘  └─┘         └─────────────────────────────────┘ └─┘ └─┘
src        └──┘   └┘     └────┘└─────────────────────────────────┘      
typ        └──┘└─┘└┘└─┘  └────┘└─────────────────────────────────┘└─┘└─┘
doc        └──┘   └┘     └────┘                                         
txt        └──┘   └┘     └────┘                                         
par        └──┘   └┘     └────┘                                         
pid          └┘   └┘                                                   
st   ─────┘└─────┘└───┘└───────────────────────────────────────────────────┘└┘
173      rw [borel_eq_generate_from_of_subbasis this],
id           └────────────────────────────────┘ └──┘
src      └──┘└────────────────────────────────┘    
typ      └──┘└────────────────────────────────┘└──┘
doc      └──┘                                      
txt      └──┘                                      
par      └──┘                                      
pid        └┘                                      
st   ──────────────────────────────────────────────┘└──
174      exact generate_from_le (assume p ⟨u, hu, v, hv, eq⟩,
id             └──────────────┘                        └┘
src      └────┘└──────────────┘       └──┘ └┘  └┘ └┘  └┘└┘└──
typ      └────┘└──────────────┘       └──┘└┘  └┘└┘  └┘└┘└──
doc      └────┘                       └──┘ └┘  └┘ └┘  └┘  └──
txt      └────┘                       └──┘ └┘  └┘ └┘  └┘  └──
par      └────┘                       └──┘ └┘  └┘ └┘  └┘  └──
pid                                  └──┘ └┘  └┘ └┘  └┘  └──
st   ─────────────────────────────────────────────────────────
175        have hu : is_open u, by rw [ha₅]; exact generate_open.basic _ hu,
id                                     └─┘         └─────────────────┘   └┘
src  ─────┘    └────┘        └───┘└──┘   └──────┘└─────────────────┘└─┘  └─
typ  ─────┘    └────┘        └───┘└──┘└─┘└──────┘└─────────────────┘└─┘└┘└─
doc  ─────┘    └────┘        └───┘└──┘   └──────┘                   └─┘  └─
txt  ─────┘    └────┘        └───┘└──┘   └──────┘                   └─┘  └─
par  ─────┘    └────┘        └───┘└──┘   └──────┘                   └─┘  └─
pid  ─────┘    └────┘        └───────┘   └───────┘                   └─┘  └─
st   ────────────────────────────┘└──────┘└──────────────────────────────┘└─
176        have hv : is_open v, by rw [hb₅]; exact generate_open.basic _ hv,
id                   └─────┘           └─┘         └─────────────────┘   └┘
src  ─────┘    └────┘└─────┘ └───┘└──┘   └──────┘└─────────────────┘└─┘  └─
typ  ─────┘    └────┘└─────┘ └───┘└──┘└─┘└──────┘└─────────────────┘└─┘└┘└─
doc  ─────┘    └────┘└─────┘ └───┘└──┘   └──────┘                   └─┘  └─
txt  ─────┘    └────┘        └───┘└──┘   └──────┘                   └─┘  └─
par  ─────┘    └────┘        └───┘└──┘   └──────┘                   └─┘  └─
pid  ─────┘    └────┘        └───────┘   └───────┘                   └─┘  └─
st   ────────────────────────────┘└──────┘└──────────────────────────────┘└─
177        eq.symm ▸ is_measurable_set_prod (is_measurable_of_is_open hu) (is_measurable_of_is_open hv))
id           └───┘  └────────────────────┘                                └──────────────────────┘
src  ─────┘  └───┘└────────────────────┘                           └┘ └──────────────────────┘  └─┘
typ  ─────┘  └───┘└────────────────────┘                           └┘ └──────────────────────┘  └─┘
doc  ─────┘                                                         └┘                           └─┘
txt  ─────┘                                                         └┘                           └─┘
par  ─────┘                                                         └┘                           └─┘
pid  ─────┘                                                         └┘                           └┘
st   ───────────────────────────────────────────────────────────────────────────────────────────────────┘
178  end
st   └─┘
179  
180  lemma measurable_of_continuous2 {α β γ}
181    [topological_space α] [second_countable_topology α]
id      └───────────────┘    └───────────────────────┘ 
src     └───────────────┘     └───────────────────────┘
typ     └───────────────┘    └───────────────────────┘ 
doc     └───────────────┘     └───────────────────────┘
182    [topological_space β] [second_countable_topology β]
id      └───────────────┘    └───────────────────────┘ 
src     └───────────────┘     └───────────────────────┘
typ     └───────────────┘    └───────────────────────┘ 
doc     └───────────────┘     └───────────────────────┘
183    [topological_space γ] [measurable_space δ] {f : δ → α} {g : δ → β} {c : α → β → γ}
id      └───────────────┘    └──────────────┘                                  
src     └───────────────┘     └──────────────┘
typ     └───────────────┘    └──────────────┘                                  
doc     └───────────────┘
184    (h : continuous (λp:α×β, c p.1 p.2)) (hf : measurable f) (hg : measurable g) :
id          └────────┘                    └────────┘         └────────┘ 
src         └────────┘                         └────────┘          └────────┘
typ         └────────┘                    └────────┘         └────────┘ 
doc         └────────┘                            └────────┘          └────────┘
185    measurable (λa, c (f a) (g a)) :=
id     └────────┘            
src    └────────┘
typ    └────────┘            
doc    └────────┘
186  show measurable ((λp:α×β, c p.1 p.2) ∘ (λa, (f a, g a))),
id        └────────┘                       
src       └────────┘                         
typ       └────────┘                       
doc       └────────┘
187  begin
st   └─────
188    apply measurable.comp,
id           └─────────────┘
src    └────┘└─────────────┘
typ    └────┘└─────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ──────────────────────┘└─
189    { rw borel_prod,
id          └────────┘
src      └─┘└────────┘
typ      └─┘└────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ───┘└───────────┘└─
190      exact measurable_of_continuous h },
id             └──────────────────────┘ 
src      └────┘└──────────────────────┘ 
typ      └────┘└──────────────────────┘
doc      └────┘                         
txt      └────┘                         
par      └────┘                         
pid                                    
st   ────────────────────────────────────┘└┘
191    { exact measurable.prod_mk hf hg }
id             └────────────────┘ └┘ └┘
src      └────┘└────────────────┘    
typ      └────┘└────────────────┘└┘└┘
doc      └────┘                      
txt      └────┘                      
par      └────┘                      
pid                                 
st   ──────────────────────────────────┘└─
192  end
st   ──┘
193  
194  lemma measurable.add
195    [add_monoid α] [topological_add_monoid α] [second_countable_topology α] [measurable_space β]
id      └────────┘    └────────────────────┘    └───────────────────────┘    └──────────────┘ 
src     └────────┘     └────────────────────┘     └───────────────────────┘     └──────────────┘
typ     └────────┘    └────────────────────┘    └───────────────────────┘    └──────────────┘ 
doc                    └────────────────────┘     └───────────────────────┘
196    {f : β → α} {g : β → α} : measurable f → measurable g → measurable (λa, f a + g a) :=
id                           └────────┘    └────────┘    └────────┘         
src                              └────────┘     └────────┘     └────────┘          
typ                          └────────┘    └────────┘    └────────┘         
doc                              └────────┘     └────────┘     └────────┘
197  measurable_of_continuous2 continuous_add
id   └───────────────────────┘ └────────────┘
src  └───────────────────────┘ └────────────┘
typ  └───────────────────────┘ └────────────┘
198  
199  lemma measurable_finset_sum {ι : Type*}
200    [add_comm_monoid α] [topological_add_monoid α] [second_countable_topology α] [measurable_space β]
id      └─────────────┘    └────────────────────┘    └───────────────────────┘    └──────────────┘ 
src     └─────────────┘     └────────────────────┘     └───────────────────────┘     └──────────────┘
typ     └─────────────┘    └────────────────────┘    └───────────────────────┘    └──────────────┘ 
doc                         └────────────────────┘     └───────────────────────┘
201    {f : ι → β → α} (s : finset ι) (hf : ∀i, measurable (f i)) : measurable (λa, s.sum (λi, f i a)) :=
id                       └────┘            └────────┘        └────────┘     └──┘       
src                         └────┘              └────────┘          └────────┘       └──┘
typ                      └────┘            └────────┘        └────────┘     └──┘       
doc                         └────┘              └────────┘          └────────┘
202  finset.induction_on s
id   └─────────────────┘ 
src  └─────────────────┘
typ  └─────────────────┘ 
doc  └─────────────────┘
203    (by simpa using measurable_const)
id                     └──────────────┘
src        └──────────┘└──────────────┘
typ        └──────────┘└──────────────┘
doc        └──────────┘
txt        └──────────┘
par        └──────────┘
pid             └────┘
st        └───────────────────────────┘
204    (assume i s his ih, by simpa [his] using measurable.add (hf i) ih)
id               └─┘ └┘            └─┘        └────────────┘  └┘   └┘
src                           └─────┘   └──────┘└────────────┘    └┘
typ              └─┘ └┘     └─────┘└─┘└──────┘└────────────┘ └┘└┘└┘
doc                           └─────┘   └──────┘                  └┘
txt                           └─────┘   └──────┘                  └┘
par                           └─────┘   └──────┘                  └┘
pid                                   └────┘                  └┘
st                           └─────────────────────────────────────────┘
205  
206  lemma measurable.neg
207    [add_group α] [topological_add_group α] [measurable_space β] {f : β → α}
id      └───────┘    └───────────────────┘    └──────────────┘           
src     └───────┘     └───────────────────┘     └──────────────┘
typ     └───────┘    └───────────────────┘    └──────────────┘           
doc                   └───────────────────┘
208    (hf : measurable f) : measurable (λa, - f a) :=
id           └────────┘     └────────┘       
src          └────────┘      └────────┘      
typ          └────────┘     └────────┘       
doc          └────────┘      └────────┘
209  (measurable_of_continuous continuous_neg).comp hf
id    └──────────────────────┘ └────────────┘ └──┘  └┘
src   └──────────────────────┘ └────────────┘ └──┘
typ   └──────────────────────┘ └────────────┘ └──┘  └┘
210  
211  lemma measurable_neg_iff
212    [add_group α] [topological_add_group α] [measurable_space β] (f : β → α) :
id      └───────┘    └───────────────────┘    └──────────────┘           
src     └───────┘     └───────────────────┘     └──────────────┘
typ     └───────┘    └───────────────────┘    └──────────────┘           
doc                   └───────────────────┘
213    measurable (λa, -f a) ↔ measurable f :=
id     └────────┘         └────────┘ 
src    └────────┘            └────────┘
typ    └────────┘         └────────┘ 
doc    └────────┘              └────────┘
214  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
215  begin
st   └─────
216    assume h,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid    └──────┘
st   ─────────┘└─
217    have := measurable.neg h,
id             └────────────┘ 
src    └──────┘└────────────┘
typ    └──────┘└────────────┘
doc    └──────┘              
txt    └──────┘              
par    └──────┘              
pid    └───┘└─┘              
st   ─────────────────────────┘└─
218    convert this,
id             └──┘
src    └──────┘
typ    └──────┘└──┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid           
st   ─────────────┘└─
219    funext,
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
st   ───────┘└─
220    simp only [pi.neg_apply, _root_.neg_neg]
id                └──────────┘  └────────────┘
src    └─────────┘└──────────┘└┘└────────────┘└┘
typ    └─────────┘└──────────┘└┘└────────────┘└┘
doc    └─────────┘            └┘              └┘
txt    └─────────┘            └┘              └┘
par    └─────────┘            └┘              └┘
pid        └──┘└┘            └┘              
st   ──────────────────────────────────────────┘
221  end
st   └─┘
222  $ measurable.neg
id     └────────────┘
src    └────────────┘
typ    └────────────┘
223  
224  lemma measurable.sub
225    [add_group α] [topological_add_group α] [second_countable_topology α] [measurable_space β]
id      └───────┘    └───────────────────┘    └───────────────────────┘    └──────────────┘ 
src     └───────┘     └───────────────────┘     └───────────────────────┘     └──────────────┘
typ     └───────┘    └───────────────────┘    └───────────────────────┘    └──────────────┘ 
doc                   └───────────────────┘     └───────────────────────┘
226    {f : β → α} {g : β → α} : measurable f → measurable g → measurable (λa, f a - g a) :=
id                           └────────┘    └────────┘    └────────┘         
src                              └────────┘     └────────┘     └────────┘          
typ                          └────────┘    └────────┘    └────────┘         
doc                              └────────┘     └────────┘     └────────┘
227  measurable_of_continuous2 continuous_sub
id   └───────────────────────┘ └────────────┘
src  └───────────────────────┘ └────────────┘
typ  └───────────────────────┘ └────────────┘
228  
229  lemma measurable.mul
230    [monoid α] [topological_monoid α] [second_countable_topology α] [measurable_space β]
id      └────┘    └────────────────┘    └───────────────────────┘    └──────────────┘ 
src     └────┘     └────────────────┘     └───────────────────────┘     └──────────────┘
typ     └────┘    └────────────────┘    └───────────────────────┘    └──────────────┘ 
doc                └────────────────┘     └───────────────────────┘
231    {f : β → α} {g : β → α} : measurable f → measurable g → measurable (λa, f a * g a) :=
id                           └────────┘    └────────┘    └────────┘         
src                              └────────┘     └────────┘     └────────┘          
typ                          └────────┘    └────────┘    └────────┘         
doc                              └────────┘     └────────┘     └────────┘
232  measurable_of_continuous2 continuous_mul
id   └───────────────────────┘ └────────────┘
src  └───────────────────────┘ └────────────┘
typ  └───────────────────────┘ └────────────┘
233  
234  lemma is_measurable_le {α β}
235    [topological_space α] [partial_order α] [order_closed_topology α] [second_countable_topology α]
id      └───────────────┘    └───────────┘    └───────────────────┘    └───────────────────────┘ 
src     └───────────────┘     └───────────┘     └───────────────────┘     └───────────────────────┘
typ     └───────────────┘    └───────────┘    └───────────────────┘    └───────────────────────┘ 
doc     └───────────────┘                       └───────────────────┘     └───────────────────────┘
236    [measurable_space β] {f : β → α} {g : β → α} (hf : measurable f) (hg : measurable g) :
id      └──────────────┘                             └────────┘         └────────┘ 
src     └──────────────┘                                  └────────┘          └────────┘
typ     └──────────────┘                             └────────┘         └────────┘ 
doc                                                       └────────┘          └────────┘
237    is_measurable {a | f a ≤ g a} :=
id     └───────────┘        
src    └───────────┘         
typ    └───────────┘        
doc    └───────────┘
238  have is_measurable {p : α × α | p.1 ≤ p.2},
id        └───────────┘             
src       └───────────┘                 
typ       └───────────┘             
doc       └───────────┘
239    by rw borel_prod; exact is_measurable_of_is_closed (order_closed_topology.is_closed_le' _),
id           └────────┘        └────────────────────────┘  └─────────────────────────────────┘
src       └─┘└────────┘  └────┘└────────────────────────┘ └─────────────────────────────────┘└─┘
typ       └─┘└────────┘  └────┘└────────────────────────┘ └─────────────────────────────────┘└─┘
doc       └─┘            └────┘                                                              └─┘
txt       └─┘            └────┘                                                              └─┘
par       └─┘            └────┘                                                              └─┘
pid                                                                                        └─┘
st       └──────────────────────────────────────────────────────────────────────────────────────┘
240  show is_measurable {a | (f a, g a).1 ≤ (f a, g a).2},
id        └───────────┘                 
src       └───────────┘                          
typ       └───────────┘                 
doc       └───────────┘
241  begin
st   └─────
242    refine measurable.preimage _ this,
id            └─────────────────┘   └──┘
src    └─────┘└─────────────────┘└─┘
typ    └─────┘└─────────────────┘└─┘└──┘
doc    └─────┘                   └─┘
txt    └─────┘                   └─┘
par    └─────┘                   └─┘
pid                             └─┘
st   ──────────────────────────────────┘└─
243    exact measurable.prod_mk hf hg
id           └────────────────┘ └┘ └┘
src    └────┘└────────────────┘    
typ    └────┘└────────────────┘└┘└┘
doc    └────┘                      
txt    └────┘                      
par    └────┘                      
pid                               
st   ────────────────────────────────┘
244  end
st   └─┘
245  
246  lemma measurable.max {α β}
247    [topological_space α] [decidable_linear_order α] [order_closed_topology α] [second_countable_topology α]
id      └───────────────┘    └────────────────────┘    └───────────────────┘    └───────────────────────┘ 
src     └───────────────┘     └────────────────────┘     └───────────────────┘     └───────────────────────┘
typ     └───────────────┘    └────────────────────┘    └───────────────────┘    └───────────────────────┘ 
doc     └───────────────┘                                └───────────────────┘     └───────────────────────┘
248    [measurable_space β] {f : β → α} {g : β → α} (hf : measurable f) (hg : measurable g) :
id      └──────────────┘                             └────────┘         └────────┘ 
src     └──────────────┘                                  └────────┘          └────────┘
typ     └──────────────┘                             └────────┘         └────────┘ 
doc                                                       └────────┘          └────────┘
249    measurable (λa, max (f a) (g a)) :=
id     └────────┘     └─┘       
src    └────────┘      └─┘
typ    └────────┘     └─┘       
doc    └────────┘
250  measurable.if (is_measurable_le hf hg) hg hf
id   └───────────┘  └──────────────┘ └┘ └┘  └┘ └┘
src  └───────────┘  └──────────────┘
typ  └───────────┘  └──────────────┘ └┘ └┘  └┘ └┘
251  
252  lemma measurable.min {α β}
253    [topological_space α] [decidable_linear_order α] [order_closed_topology α] [second_countable_topology α]
id      └───────────────┘    └────────────────────┘    └───────────────────┘    └───────────────────────┘ 
src     └───────────────┘     └────────────────────┘     └───────────────────┘     └───────────────────────┘
typ     └───────────────┘    └────────────────────┘    └───────────────────┘    └───────────────────────┘ 
doc     └───────────────┘                                └───────────────────┘     └───────────────────────┘
254    [measurable_space β] {f : β → α} {g : β → α} (hf : measurable f) (hg : measurable g) :
id      └──────────────┘                             └────────┘         └────────┘ 
src     └──────────────┘                                  └────────┘          └────────┘
typ     └──────────────┘                             └────────┘         └────────┘ 
doc                                                       └────────┘          └────────┘
255    measurable (λa, min (f a) (g a)) :=
id     └────────┘     └─┘       
src    └────────┘      └─┘
typ    └────────┘     └─┘       
doc    └────────┘
256  measurable.if (is_measurable_le hf hg) hf hg
id   └───────────┘  └──────────────┘ └┘ └┘  └┘ └┘
src  └───────────┘  └──────────────┘
typ  └───────────┘  └──────────────┘ └┘ └┘  └┘ └┘
257  
258  -- generalize
259  lemma measurable_coe_int_real : measurable (λa, a : ℤ → ℝ) :=
id                                   └────────┘           
src                                  └────────┘             
typ                                  └────────┘           
doc                                  └────────┘
260  assume s (hs : is_measurable s), by trivial
id                 └───────────┘ 
src                 └───────────┘        └───────
typ                └───────────┘       └───────
doc                 └───────────┘        └───────
txt                                      └───────
par                                      └───────
pid                                             
st                                      └────────
261  
src  
typ  
doc  
txt  
par  
pid  
st   
262  section order_closed_topology
263  variables [linear_order α] [order_closed_topology α] {a b c : α}
id              └──────────┘     └───────────────────┘
src             └──────────┘     └───────────────────┘
typ             └──────────┘     └───────────────────┘
doc                              └───────────────────┘
264  
265  lemma is_measurable_Iio : is_measurable (Iio a) := is_measurable_of_is_open is_open_Iio
id                             └───────────┘  └─┘      └──────────────────────┘ └─────────┘
src                            └───────────┘  └─┘       └──────────────────────┘ └─────────┘
typ                            └───────────┘  └─┘      └──────────────────────┘ └─────────┘
doc                            └───────────┘  └─┘
266  lemma is_measurable_Ioi : is_measurable (Ioi a) := is_measurable_of_is_open is_open_Ioi
id                             └───────────┘  └─┘      └──────────────────────┘ └─────────┘
src                            └───────────┘  └─┘       └──────────────────────┘ └─────────┘
typ                            └───────────┘  └─┘      └──────────────────────┘ └─────────┘
doc                            └───────────┘  └─┘
267  lemma is_measurable_Ici : is_measurable (Ici a) := is_measurable_of_is_closed is_closed_Ici
id                             └───────────┘  └─┘      └────────────────────────┘ └───────────┘
src                            └───────────┘  └─┘       └────────────────────────┘ └───────────┘
typ                            └───────────┘  └─┘      └────────────────────────┘ └───────────┘
doc                            └───────────┘  └─┘
268  lemma is_measurable_Iic : is_measurable (Iic a) := is_measurable_of_is_closed is_closed_Iic
id                             └───────────┘  └─┘      └────────────────────────┘ └───────────┘
src                            └───────────┘  └─┘       └────────────────────────┘ └───────────┘
typ                            └───────────┘  └─┘      └────────────────────────┘ └───────────┘
doc                            └───────────┘  └─┘
269  lemma is_measurable_Ioo : is_measurable (Ioo a b) := is_measurable_of_is_open is_open_Ioo
id                             └───────────┘  └─┘       └──────────────────────┘ └─────────┘
src                            └───────────┘  └─┘         └──────────────────────┘ └─────────┘
typ                            └───────────┘  └─┘       └──────────────────────┘ └─────────┘
doc                            └───────────┘  └─┘
270  lemma is_measurable_Ioc : is_measurable (Ioc a b) := is_measurable_Ioi.inter is_measurable_Iic
id                             └───────────┘  └─┘       └───────────────┘└────┘ └───────────────┘
src                            └───────────┘  └─┘         └───────────────┘└────┘ └───────────────┘
typ                            └───────────┘  └─┘       └───────────────┘└────┘ └───────────────┘
doc                            └───────────┘  └─┘
271  lemma is_measurable_Ico : is_measurable (Ico a b) := is_measurable_Ici.inter is_measurable_Iio
id                             └───────────┘  └─┘       └───────────────┘└────┘ └───────────────┘
src                            └───────────┘  └─┘         └───────────────┘└────┘ └───────────────┘
typ                            └───────────┘  └─┘       └───────────────┘└────┘ └───────────────┘
doc                            └───────────┘  └─┘
272  lemma is_measurable_Icc : is_measurable (Icc a b) := is_measurable_of_is_closed is_closed_Icc
id                             └───────────┘  └─┘       └────────────────────────┘ └───────────┘
src                            └───────────┘  └─┘         └────────────────────────┘ └───────────┘
typ                            └───────────┘  └─┘       └────────────────────────┘ └───────────┘
doc                            └───────────┘  └─┘
273  
274  open_locale interval
275  
276  lemma is_measurable_interval
277    {α} [decidable_linear_order α] [topological_space α] [order_closed_topology α] {a b : α} :
id          └────────────────────┘    └───────────────┘    └───────────────────┘          
src         └────────────────────┘     └───────────────┘     └───────────────────┘
typ         └────────────────────┘    └───────────────┘    └───────────────────┘          
doc                                    └───────────────┘     └───────────────────┘
278    is_measurable [a, b] :=
id     └───────────┘  
src    └───────────┘    
typ    └───────────┘  
doc    └───────────┘    
279  is_measurable_Icc
id   └───────────────┘
src  └───────────────┘
typ  └───────────────┘
280  
281  end order_closed_topology
282  
283  lemma measurable.is_lub {α} [topological_space α] [linear_order α]
id                                └───────────────┘    └──────────┘ 
src                               └───────────────┘     └──────────┘
typ                               └───────────────┘    └──────────┘ 
doc                               └───────────────┘
284    [order_topology α] [second_countable_topology α]
id      └────────────┘    └───────────────────────┘ 
src     └────────────┘     └───────────────────────┘
typ     └────────────┘    └───────────────────────┘ 
doc     └────────────┘     └───────────────────────┘
285    {β} [measurable_space β] {ι} [encodable ι]
id          └──────────────┘        └───────┘ 
src         └──────────────┘         └───────┘
typ         └──────────────┘        └───────┘ 
doc                                  └───────┘
286    {f : ι → β → α} {g : β → α} (hf : ∀ i, measurable (f i))
id                                      └────────┘   
src                                           └────────┘
typ                                     └────────┘   
doc                                           └────────┘
287    (hg : ∀ b, is_lub {a | ∃ i, f i b = a} (g b)) :
id               └────┘              
src               └────┘              
typ              └────┘              
doc               └────┘
288    measurable g :=
id     └────────┘ 
src    └────────┘
typ    └────────┘ 
doc    └────────┘
289  begin
st   └─────
290    rw borel_eq_generate_Ioi α,
id        └───────────────────┘ 
src    └─┘└───────────────────┘
typ    └─┘└───────────────────┘
doc    └─┘                     
txt    └─┘                     
par    └─┘                     
pid                           
st   ───────────────────────────┘└─
291    apply measurable_generate_from,
id           └──────────────────────┘
src    └────┘└──────────────────────┘
typ    └────┘└──────────────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ───────────────────────────────┘└─
292    rintro _ ⟨a, rfl⟩,
src    └───────────────┘
typ    └───────────────┘
doc    └───────────────┘
txt    └───────────────┘
par    └───────────────┘
pid          └─────────┘
st   ──────────────────┘└─
293    have : {b | a < g b} = ⋃ i, {b | a < f i b},
id                                   
src    └─────┘ └──┘   └┘└┘└──┘     
typ    └─────┘ └──┘  └┘└┘└──┘   
doc    └─────┘ └──┘    └┘ └┘ └──┘     
txt    └─────┘ └──┘    └┘  └┘  └──┘     
par    └─────┘ └──┘    └┘  └┘  └──┘     
pid    └───┘└┘ └──┘    └┘  └┘  └──┘     
st   ────────────────────────────────────────────┘└─
294    { simp [set.ext_iff], intro b, rw [lt_is_lub_iff (hg b)],
id             └─────────┘                └───────────┘  └┘ 
src      └────┘└─────────┘  └─────┘  └──┘└───────────┘    └┘
typ      └────┘└─────────┘  └─────┘  └──┘└───────────┘ └┘└┘
doc      └────┘             └─────┘  └──┘                 └┘
txt      └────┘             └─────┘  └──┘                 └┘
par      └────┘             └─────┘  └──┘                 └┘
pid                            └┘    └┘                 └┘
st   ───┘└────────────────┘└───────┘└────────────────────────┘└──
295      exact ⟨λ ⟨_, ⟨i, rfl⟩, h⟩, ⟨i, h⟩, λ ⟨i, h⟩, ⟨_, ⟨i, rfl⟩, h⟩⟩ },
id                                                        └─┘
src      └────┘  └───┘  └┘   └─┘ └─┘  └┘ └─┘ └┘ └┘ └─┘ └─┘  └┘└─┘└─┘ └─┘
typ      └────┘  └───┘ └┘   └─┘└─┘  └┘ └─┘ └┘└┘└─┘ └─┘  └┘└─┘└─┘ └─┘
doc      └────┘  └───┘  └┘   └─┘ └─┘  └┘ └─┘ └┘ └┘ └─┘ └─┘  └┘   └─┘ └─┘
txt      └────┘  └───┘  └┘   └─┘ └─┘  └┘ └─┘ └┘ └┘ └─┘ └─┘  └┘   └─┘ └─┘
par      └────┘  └───┘  └┘   └─┘ └─┘  └┘ └─┘ └┘ └┘ └─┘ └─┘  └┘   └─┘ └─┘
pid             └───┘  └┘   └─┘ └─┘  └┘ └─┘ └┘ └┘ └─┘ └─┘  └┘   └─┘ └┘
st   ──────────────────────────────────────────────────────────────────┘└┘
296    show is_measurable {b | a < g b}, rw this,
id          └───────────┘                └──┘
src    └───┘└───────────┘└──┘      └─┘
typ    └───┘└───────────┘└──┘    └─┘└──┘
doc    └───┘└───────────┘ └──┘      └─┘
txt    └───┘              └──┘      └─┘
par    └───┘              └──┘      └─┘
pid    └───┘              └──┘        
st   ─────────────────────────────────┘└───────┘└─
297    exact is_measurable.Union (λ i, hf i _
id           └─────────────────┘       └┘
src    └────┘└─────────────────┘  └──┘   └──
typ    └────┘└─────────────────┘  └──┘└┘ └──
doc    └────┘                     └──┘   └──
txt    └────┘                     └──┘   └──
par    └────┘                     └──┘   └──
pid                              └──┘   └──
st   ─────────────────────────────────────────
298      (is_measurable_of_is_open (is_open_lt' _)))
id        └──────────────────────┘  └─────────┘
src  ───┘ └──────────────────────┘ └─────────┘└────┘
typ  ───┘ └──────────────────────┘ └─────────┘└────┘
doc  ───┘                                     └────┘
txt  ───┘                                     └────┘
par  ───┘                                     └────┘
pid  ───┘                                     └───┘
st   ───────────────────────────────────────────────┘
299  end
st   └─┘
300  
301  lemma measurable.is_glb {α} [topological_space α] [linear_order α]
id                                └───────────────┘    └──────────┘ 
src                               └───────────────┘     └──────────┘
typ                               └───────────────┘    └──────────┘ 
doc                               └───────────────┘
302    [order_topology α] [second_countable_topology α]
id      └────────────┘    └───────────────────────┘ 
src     └────────────┘     └───────────────────────┘
typ     └────────────┘    └───────────────────────┘ 
doc     └────────────┘     └───────────────────────┘
303    {β} [measurable_space β] {ι} [encodable ι]
id          └──────────────┘        └───────┘ 
src         └──────────────┘         └───────┘
typ         └──────────────┘        └───────┘ 
doc                                  └───────┘
304    {f : ι → β → α} {g : β → α} (hf : ∀ i, measurable (f i))
id                                      └────────┘   
src                                           └────────┘
typ                                     └────────┘   
doc                                           └────────┘
305    (hg : ∀ b, is_glb {a | ∃ i, f i b = a} (g b)) :
id               └────┘              
src               └────┘              
typ              └────┘              
doc               └────┘
306    measurable g :=
id     └────────┘ 
src    └────────┘
typ    └────────┘ 
doc    └────────┘
307  begin
st   └─────
308    rw borel_eq_generate_Iio α,
id        └───────────────────┘ 
src    └─┘└───────────────────┘
typ    └─┘└───────────────────┘
doc    └─┘                     
txt    └─┘                     
par    └─┘                     
pid                           
st   ───────────────────────────┘└─
309    apply measurable_generate_from,
id           └──────────────────────┘
src    └────┘└──────────────────────┘
typ    └────┘└──────────────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ───────────────────────────────┘└─
310    rintro _ ⟨a, rfl⟩,
src    └───────────────┘
typ    └───────────────┘
doc    └───────────────┘
txt    └───────────────┘
par    └───────────────┘
pid          └─────────┘
st   ──────────────────┘└─
311    have : {b | g b < a} = ⋃ i, {b | f i b < a},
id                                       
src    └─────┘ └──┘   └┘└┘└──┘     
typ    └─────┘ └──┘  └┘└┘└──┘   
doc    └─────┘ └──┘    └┘ └┘ └──┘     
txt    └─────┘ └──┘    └┘  └┘  └──┘     
par    └─────┘ └──┘    └┘  └┘  └──┘     
pid    └───┘└┘ └──┘    └┘  └┘  └──┘     
st   ────────────────────────────────────────────┘└─
312    { simp [set.ext_iff], intro b, rw [is_glb_lt_iff (hg b)],
id             └─────────┘                └───────────┘  └┘ 
src      └────┘└─────────┘  └─────┘  └──┘└───────────┘    └┘
typ      └────┘└─────────┘  └─────┘  └──┘└───────────┘ └┘└┘
doc      └────┘             └─────┘  └──┘                 └┘
txt      └────┘             └─────┘  └──┘                 └┘
par      └────┘             └─────┘  └──┘                 └┘
pid                            └┘    └┘                 └┘
st   ───┘└────────────────┘└───────┘└────────────────────────┘└──
313      exact ⟨λ ⟨_, ⟨i, rfl⟩, h⟩, ⟨i, h⟩, λ ⟨i, h⟩, ⟨_, ⟨i, rfl⟩, h⟩⟩ },
id                                                        └─┘
src      └────┘  └───┘  └┘   └─┘ └─┘  └┘ └─┘ └┘ └┘ └─┘ └─┘  └┘└─┘└─┘ └─┘
typ      └────┘  └───┘ └┘   └─┘└─┘  └┘ └─┘ └┘└┘└─┘ └─┘  └┘└─┘└─┘ └─┘
doc      └────┘  └───┘  └┘   └─┘ └─┘  └┘ └─┘ └┘ └┘ └─┘ └─┘  └┘   └─┘ └─┘
txt      └────┘  └───┘  └┘   └─┘ └─┘  └┘ └─┘ └┘ └┘ └─┘ └─┘  └┘   └─┘ └─┘
par      └────┘  └───┘  └┘   └─┘ └─┘  └┘ └─┘ └┘ └┘ └─┘ └─┘  └┘   └─┘ └─┘
pid             └───┘  └┘   └─┘ └─┘  └┘ └─┘ └┘ └┘ └─┘ └─┘  └┘   └─┘ └┘
st   ──────────────────────────────────────────────────────────────────┘└┘
314    show is_measurable {b | g b < a}, rw this,
id          └───────────┘                └──┘
src    └───┘└───────────┘└──┘      └─┘
typ    └───┘└───────────┘└──┘    └─┘└──┘
doc    └───┘└───────────┘ └──┘      └─┘
txt    └───┘              └──┘      └─┘
par    └───┘              └──┘      └─┘
pid    └───┘              └──┘        
st   ─────────────────────────────────┘└───────┘└─
315    exact is_measurable.Union (λ i, hf i _
id           └─────────────────┘       └┘
src    └────┘└─────────────────┘  └──┘   └──
typ    └────┘└─────────────────┘  └──┘└┘ └──
doc    └────┘                     └──┘   └──
txt    └────┘                     └──┘   └──
par    └────┘                     └──┘   └──
pid                              └──┘   └──
st   ─────────────────────────────────────────
316      (is_measurable_of_is_open (is_open_gt' _)))
id        └──────────────────────┘  └─────────┘
src  ───┘ └──────────────────────┘ └─────────┘└────┘
typ  ───┘ └──────────────────────┘ └─────────┘└────┘
doc  ───┘                                     └────┘
txt  ───┘                                     └────┘
par  ───┘                                     └────┘
pid  ───┘                                     └───┘
st   ───────────────────────────────────────────────┘
317  end
st   └─┘
318  
319  lemma measurable.supr {α} [topological_space α] [complete_linear_order α]
id                              └───────────────┘    └───────────────────┘ 
src                             └───────────────┘     └───────────────────┘
typ                             └───────────────┘    └───────────────────┘ 
doc                             └───────────────┘     └───────────────────┘
320    [order_topology α] [second_countable_topology α]
id      └────────────┘    └───────────────────────┘ 
src     └────────────┘     └───────────────────────┘
typ     └────────────┘    └───────────────────────┘ 
doc     └────────────┘     └───────────────────────┘
321    {β} [measurable_space β] {ι} [encodable ι]
id          └──────────────┘        └───────┘ 
src         └──────────────┘         └───────┘
typ         └──────────────┘        └───────┘ 
doc                                  └───────┘
322    {f : ι → β → α} (hf : ∀ i, measurable (f i)) :
id                            └────────┘   
src                               └────────┘
typ                           └────────┘   
doc                               └────────┘
323    measurable (λ b, ⨆ i, f i b) :=
id     └────────┘          
src    └────────┘         
typ    └────────┘          
doc    └────────┘         
324  measurable.is_lub hf $ λ b, is_lub_supr
id   └───────────────┘ └┘       └─────────┘
src  └───────────────┘           └─────────┘
typ  └───────────────┘ └┘       └─────────┘
325  
326  lemma measurable.infi {α} [topological_space α] [complete_linear_order α]
id                              └───────────────┘    └───────────────────┘ 
src                             └───────────────┘     └───────────────────┘
typ                             └───────────────┘    └───────────────────┘ 
doc                             └───────────────┘     └───────────────────┘
327    [order_topology α] [second_countable_topology α]
id      └────────────┘    └───────────────────────┘ 
src     └────────────┘     └───────────────────────┘
typ     └────────────┘    └───────────────────────┘ 
doc     └────────────┘     └───────────────────────┘
328    {β} [measurable_space β] {ι} [encodable ι]
id          └──────────────┘        └───────┘ 
src         └──────────────┘         └───────┘
typ         └──────────────┘        └───────┘ 
doc                                  └───────┘
329    {f : ι → β → α} (hf : ∀ i, measurable (f i)) :
id                            └────────┘   
src                               └────────┘
typ                           └────────┘   
doc                               └────────┘
330    measurable (λ b, ⨅ i, f i b) :=
id     └────────┘          
src    └────────┘         
typ    └────────┘          
doc    └────────┘         
331  measurable.is_glb hf $ λ b, is_glb_infi
id   └───────────────┘ └┘       └─────────┘
src  └───────────────┘           └─────────┘
typ  └───────────────┘ └┘       └─────────┘
332  
333  lemma measurable.supr_Prop {α} [topological_space α] [complete_linear_order α]
id                                   └───────────────┘    └───────────────────┘ 
src                                  └───────────────┘     └───────────────────┘
typ                                  └───────────────┘    └───────────────────┘ 
doc                                  └───────────────┘     └───────────────────┘
334    {β} [measurable_space β] {p : Prop} {f : β → α} (hf : measurable f) :
id          └──────────────┘                              └────────┘ 
src         └──────────────┘                                 └────────┘
typ         └──────────────┘                              └────────┘ 
doc                                                          └────────┘
335    measurable (λ b, ⨆ h : p, f b) :=
id     └────────┘             
src    └────────┘             
typ    └────────┘             
doc    └────────┘             
336  classical.by_cases
id   └────────────────┘
src  └────────────────┘
typ  └────────────────┘
337    (assume h : p, begin convert hf, funext, exact supr_pos h end)
id                                 └┘                └──────┘ 
src                         └──────┘    └────┘  └────┘└──────┘ 
typ                        └──────┘└┘  └────┘  └────┘└──────┘
doc                         └──────┘    └────┘  └────┘         
txt                         └──────┘    └────┘  └────┘         
par                         └──────┘    └────┘  └────┘         
pid                                                          
st                    └──────────────┘└──────┘└─────────────────┘└─┘
338    (assume h : ¬p, begin convert measurable_const, funext, exact supr_neg h end)
id                                 └──────────────┘                └──────┘ 
src                         └──────┘└──────────────┘  └────┘  └────┘└──────┘ 
typ                        └──────┘└──────────────┘  └────┘  └────┘└──────┘
doc                          └──────┘                  └────┘  └────┘         
txt                          └──────┘                  └────┘  └────┘         
par                          └──────┘                  └────┘  └────┘         
pid                                                                         
st                     └────────────────────────────┘└──────┘└─────────────────┘└─┘
339  
340  lemma measurable.infi_Prop {α} [topological_space α] [complete_linear_order α]
id                                   └───────────────┘    └───────────────────┘ 
src                                  └───────────────┘     └───────────────────┘
typ                                  └───────────────┘    └───────────────────┘ 
doc                                  └───────────────┘     └───────────────────┘
341    {β} [measurable_space β] {p : Prop} {f : β → α} (hf : measurable f) :
id          └──────────────┘                              └────────┘ 
src         └──────────────┘                                 └────────┘
typ         └──────────────┘                              └────────┘ 
doc                                                          └────────┘
342    measurable (λ b, ⨅ h : p, f b) :=
id     └────────┘             
src    └────────┘             
typ    └────────┘             
doc    └────────┘             
343  classical.by_cases
id   └────────────────┘
src  └────────────────┘
typ  └────────────────┘
344    (assume h : p, begin convert hf, funext, exact infi_pos h end )
id                                 └┘                └──────┘ 
src                         └──────┘    └────┘  └────┘└──────┘ 
typ                        └──────┘└┘  └────┘  └────┘└──────┘
doc                         └──────┘    └────┘  └────┘         
txt                         └──────┘    └────┘  └────┘         
par                         └──────┘    └────┘  └────┘         
pid                                                          
st                    └──────────────┘└──────┘└─────────────────┘└─┘
345    (assume h : ¬p, begin convert measurable_const, funext, exact infi_neg h end)
id                                 └──────────────┘                └──────┘ 
src                         └──────┘└──────────────┘  └────┘  └────┘└──────┘ 
typ                        └──────┘└──────────────┘  └────┘  └────┘└──────┘
doc                          └──────┘                  └────┘  └────┘         
txt                          └──────┘                  └────┘  └────┘         
par                          └──────┘                  └────┘  └────┘         
pid                                                                         
st                     └────────────────────────────┘└──────┘└─────────────────┘└─┘
346  
347  end
348  
349  def homemorph.to_measurable_equiv [topological_space α] [topological_space β] (h : α ≃ₜ β) :
id                                      └───────────────┘    └───────────────┘         └┘ 
src                                     └───────────────┘     └───────────────┘           └┘
typ                                     └───────────────┘    └───────────────┘         └┘ 
doc                                     └───────────────┘     └───────────────┘           └┘
350    measurable_equiv α β :=
id     └──────────────┘  
src    └──────────────┘
typ    └──────────────┘  
doc    └──────────────┘
351  { to_equiv := h.to_equiv,
id                 └───────┘
src                 └───────┘
typ                └───────┘
352    measurable_to_fun := measurable_of_continuous h.continuous_to_fun,
id                          └──────────────────────┘ └────────────────┘
src                         └──────────────────────┘  └────────────────┘
typ                         └──────────────────────┘ └────────────────┘
353    measurable_inv_fun := measurable_of_continuous h.continuous_inv_fun }
id                           └──────────────────────┘ └─────────────────┘
src                          └──────────────────────┘  └─────────────────┘
typ                          └──────────────────────┘ └─────────────────┘
354  
355  namespace real
356  open measurable_space
357  
358  lemma borel_eq_generate_from_Ioo_rat :
359    borel ℝ = generate_from (⋃(a b : ℚ) (h : a < b), {Ioo a b}) :=
id     └───┘   └───────────┘                    └─┘  
src    └───┘   └───────────┘                      └─┘
typ    └───┘   └───────────┘                    └─┘  
doc              └───────────┘                        └─┘
360  borel_eq_generate_from_of_subbasis is_topological_basis_Ioo_rat.2.2
id   └────────────────────────────────┘ └──────────────────────────┘ 
src  └────────────────────────────────┘ └──────────────────────────┘ 
typ  └────────────────────────────────┘ └──────────────────────────┘ 
361  
362  lemma borel_eq_generate_from_Iio_rat :
363    borel ℝ = generate_from (⋃a:ℚ, {Iio a}) :=
id     └───┘   └───────────┘     └─┘ 
src    └───┘   └───────────┘     └─┘
typ    └───┘   └───────────┘     └─┘ 
doc              └───────────┘      └─┘
364  begin
st   └─────
365    let g, swap,
src    └───┘  └──┘
typ    └───┘  └──┘
doc    └───┘  └──┘
txt    └───┘  └──┘
par    └───┘  └──┘
pid    └───┘
st   ──────┘└────┘└─
366    apply le_antisymm (_ : _ ≤ g) (measurable_space.generate_from_le (λ t, _)),
id           └─────────┘            └───────────────────────────────┘
src    └────┘└─────────┘ └────┘ └┘ └───────────────────────────────┘  └─────┘
typ    └────┘└─────────┘ └────┘└┘ └───────────────────────────────┘  └─────┘
doc    └────┘            └────┘  └┘                                    └─────┘
txt    └────┘            └────┘  └┘                                    └─────┘
par    └────┘            └────┘  └┘                                    └─────┘
pid                     └────┘  └┘                                    └─────┘
st   ───────────────────────────────────────────────────────────────────────────┘└─
367    { rw borel_eq_generate_from_Ioo_rat,
id          └────────────────────────────┘
src      └─┘└────────────────────────────┘
typ      └─┘└────────────────────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ───┘└───────────────────────────────┘└─
368      refine generate_from_le (λ t, _),
id              └──────────────┘
src      └─────┘└──────────────┘  └────┘
typ      └─────┘└──────────────┘  └────┘
doc      └─────┘                  └────┘
txt      └─────┘                  └────┘
par      └─────┘                  └────┘
pid                              └────┘
st   ───────────────────────────────────┘└─
369      simp only [mem_Union], rintro ⟨a, b, h, rfl|⟨⟨⟩⟩⟩,
id                  └───────┘
src      └─────────┘└───────┘  └────────────────────────┘
typ      └─────────┘└───────┘  └────────────────────────┘
doc      └─────────┘           └────────────────────────┘
txt      └─────────┘           └────────────────────────┘
par      └─────────┘           └────────────────────────┘
pid          └──┘└┘                 └──────────────────┘
st   ────────────────────────┘└──────────────────────────┘└─
370      rw (set.ext (λ x, _) : Ioo (a:ℝ) b = (⋃c>a, - Iio c) ∩ Iio b),
id           └─────┘            └─┘                       └─┘ 
src      └─┘ └─────┘  └───────┘└─┘   └┘  └┘     └┘└─┘ 
typ      └─┘ └─────┘  └───────┘└─┘   └┘  └┘    └┘└─┘
doc      └─┘          └───────┘└─┘   └┘   └┘      └┘ └─┘ 
txt      └─┘          └───────┘      └┘    └┘       └┘     
par      └─┘          └───────┘      └┘    └┘       └┘     
pid                  └───────┘      └┘    └┘       └┘     
st   ────────────────────────────────────────────────────────────────┘└─
371      { have hg : ∀q:ℚ, g.is_measurable (Iio q) :=
id                         └─────────────┘  └─┘
src        └────────┘ └┘  └─────────────┘ └─┘ └────
typ        └────────┘ └┘  └─────────────┘ └─┘ └────
doc        └────────┘ └┘                  └─┘ └────
txt        └────────┘ └┘                      └────
par        └────────┘ └┘                      └────
pid        └─────┘└─┘ └┘                      └───
st   ─────┘└──────────────────────────────────────────
372          λ q, generate_measurable.basic _ (by simp; exact ⟨_, rfl⟩),
id                └───────────────────────┘                       └─┘
src  ───────┘ └──┘└───────────────────────┘└─┘   └──┘└┘└────┘ └─┘└─┘
typ  ───────┘ └──┘└───────────────────────┘└─┘   └──┘└┘└────┘ └─┘└─┘
doc  ───────┘ └──┘                         └─┘   └──┘└┘└────┘ └─┘   
txt  ───────┘ └──┘                         └─┘   └──┘└┘└────┘ └─┘   
par  ───────┘ └──┘                         └─┘   └──┘└┘└────┘ └─┘   
pid  ───────┘ └──┘                         └─┘   └───────────┘ └─┘   └┘
st   ───────────────────────────────────────────┘└───────────────────┘└─
373        refine @is_measurable.inter _ g _ _ _ (hg _),
id                 └─────────────────┘           └┘
src        └─────┘ └─────────────────┘└─┘ └─────┘   └─┘
typ        └─────┘ └─────────────────┘└─┘└─────┘ └┘└─┘
doc        └─────┘                    └─┘ └─────┘   └─┘
txt        └─────┘                    └─┘ └─────┘   └─┘
par        └─────┘                    └─┘ └─────┘   └─┘
pid                                  └─┘ └─────┘   └─┘
st   ─────────────────────────────────────────────────┘└─
374        refine @is_measurable.bUnion _ _ g _ _ (countable_encodable _) (λ c h, _),
id                 └──────────────────┘           └─────────────────┘
src        └─────┘ └──────────────────┘└───┘ └───┘ └─────────────────┘└──┘  └──────┘
typ        └─────┘ └──────────────────┘└───┘└───┘ └─────────────────┘└──┘  └──────┘
doc        └─────┘                     └───┘ └───┘                    └──┘  └──────┘
txt        └─────┘                     └───┘ └───┘                    └──┘  └──────┘
par        └─────┘                     └───┘ └───┘                    └──┘  └──────┘
pid                                   └───┘ └───┘                    └──┘  └──────┘
st   ──────────────────────────────────────────────────────────────────────────────┘└─
375        exact @is_measurable.compl _ _ g (hg _) },
id                └─────────────────┘       └┘
src        └────┘ └─────────────────┘└───┘    └──┘
typ        └────┘ └─────────────────┘└───┘ └┘└──┘
doc        └────┘                    └───┘    └──┘
txt        └────┘                    └───┘    └──┘
par        └────┘                    └───┘    └──┘
pid                                 └───┘    └─┘
st   ─────────────────────────────────────────────┘└┘
376      { simp [Ioo, Iio],
id               └─┘  └─┘
src        └────┘└─┘└┘└─┘
typ        └────┘└─┘└┘└─┘
doc        └────┘└─┘└┘└─┘
txt        └────┘   └┘   
par        └────┘   └┘   
pid               └┘   
st   ────────────────────┘└─
377        refine and_congr _ iff.rfl,
id                └───────┘   └─────┘
src        └─────┘└───────┘└─┘└─────┘
typ        └─────┘└───────┘└─┘└─────┘
doc        └─────┘         └─┘
txt        └─────┘         └─┘
par        └─────┘         └─┘
pid                       └─┘
st   ───────────────────────────────┘└─
378        exact ⟨λ h,
src        └────┘  └───
typ        └────┘  └───
doc        └────┘  └───
txt        └────┘  └───
par        └────┘  └───
pid               └───
st   ──────────────────
379          let ⟨c, ac, cx⟩ := exists_rat_btwn h in
id                  └┘  └┘     └─────────────┘
src  ───────┘     └┘  └┘  └───┘└─────────────┘ └───
typ  ───────┘    └┘└┘└┘└┘└───┘└─────────────┘ └───
doc  ───────┘     └┘  └┘  └───┘                └───
txt  ───────┘     └┘  └┘  └───┘                └───
par  ───────┘     └┘  └┘  └───┘                └───
pid  ───────┘     └┘  └┘  └───┘                └───
st   ────────────────────────────────────────────────
380          ⟨c, rat.cast_lt.1 ac, le_of_lt cx⟩,
id                                 └──────┘
src  ───────┘  └┘           └─┘  └┘└──────┘  └──
typ  ───────┘  └┘           └─┘  └┘└──────┘  └──
doc  ───────┘  └┘           └─┘  └┘          └──
txt  ───────┘  └┘           └─┘  └┘          └──
par  ───────┘  └┘           └─┘  └┘          └──
pid  ───────┘  └┘           └─┘  └┘          └──
st   ────────────────────────────────────────────
381         λ ⟨c, ac, cx⟩, lt_of_lt_of_le (rat.cast_lt.2 ac) cx⟩ } },
id                └┘  └┘   └────────────┘  └─────────┘
src  ──────┘ └┘ └┘  └┘  └─┘└────────────┘ └─────────┘└─┘  └┘  └┘
typ  ──────┘ └┘ └┘└┘└┘└┘└─┘└────────────┘ └─────────┘└─┘  └┘  └┘
doc  ──────┘ └┘ └┘  └┘  └─┘                          └─┘  └┘  └┘
txt  ──────┘ └┘ └┘  └┘  └─┘                          └─┘  └┘  └┘
par  ──────┘ └┘ └┘  └┘  └─┘                          └─┘  └┘  └┘
pid  ──────┘ └┘ └┘  └┘  └─┘                          └─┘  └┘  
st   ───────────────────────────────────────────────────────────┘└──┘
382    { simp, rintro r rfl,
src      └──┘  └──────────┘
typ      └──┘  └──────────┘
doc      └──┘  └──────────┘
txt      └──┘  └──────────┘
par      └──┘  └──────────┘
pid                  └────┘
st   ───────┘└────────────┘└─
383      exact is_measurable_of_is_open (is_open_gt' _) }
id             └──────────────────────┘  └─────────┘
src      └────┘└──────────────────────┘ └─────────┘└──┘
typ      └────┘└──────────────────────┘ └─────────┘└──┘
doc      └────┘                                    └──┘
txt      └────┘                                    └──┘
par      └────┘                                    └──┘
pid                                               └─┘
st   ──────────────────────────────────────────────────┘└─
384  end
st   ──┘
385  
386  end real
387  
388  namespace nnreal
389  open filter
390  
391  lemma measurable.add [measurable_space α] {f : α → nnreal} {g : α → nnreal} :
id                         └──────────────┘           └────┘          └────┘
src                        └──────────────┘             └────┘           └────┘
typ                        └──────────────┘           └────┘          └────┘
doc                                                     └────┘           └────┘
392    measurable f → measurable g → measurable (λa, f a + g a) :=
id     └────────┘    └────────┘    └────────┘         
src    └────────┘     └────────┘     └────────┘          
typ    └────────┘    └────────┘    └────────┘         
doc    └────────┘     └────────┘     └────────┘
393  measurable_of_continuous2 continuous_add
id   └───────────────────────┘ └────────────┘
src  └───────────────────────┘ └────────────┘
typ  └───────────────────────┘ └────────────┘
394  
395  lemma measurable.sub [measurable_space α] {f g: α → nnreal}
id                         └──────────────┘            └────┘
src                        └──────────────┘              └────┘
typ                        └──────────────┘            └────┘
doc                                                      └────┘
396    (hf : measurable f) (hg : measurable g) : measurable (λ a, f a - g a) :=
id           └────────┘         └────────┘     └────────┘          
src          └────────┘          └────────┘      └────────┘           
typ          └────────┘         └────────┘     └────────┘          
doc          └────────┘          └────────┘      └────────┘
397  measurable_of_continuous2 continuous_sub hf hg
id   └───────────────────────┘ └────────────┘ └┘ └┘
src  └───────────────────────┘ └────────────┘
typ  └───────────────────────┘ └────────────┘ └┘ └┘
398  
399  lemma measurable.mul [measurable_space α] {f : α → nnreal} {g : α → nnreal} :
id                         └──────────────┘           └────┘          └────┘
src                        └──────────────┘             └────┘           └────┘
typ                        └──────────────┘           └────┘          └────┘
doc                                                     └────┘           └────┘
400    measurable f → measurable g → measurable (λa, f a * g a) :=
id     └────────┘    └────────┘    └────────┘         
src    └────────┘     └────────┘     └────────┘          
typ    └────────┘    └────────┘    └────────┘         
doc    └────────┘     └────────┘     └────────┘
401  measurable_of_continuous2 continuous_mul
id   └───────────────────────┘ └────────────┘
src  └───────────────────────┘ └────────────┘
typ  └───────────────────────┘ └────────────┘
402  
403  lemma measurable_of_real : measurable nnreal.of_real :=
id                              └────────┘ └────────────┘
src                             └────────┘ └────────────┘
typ                             └────────┘ └────────────┘
doc                             └────────┘
404  measurable_of_continuous nnreal.continuous_of_real
id   └──────────────────────┘ └───────────────────────┘
src  └──────────────────────┘ └───────────────────────┘
typ  └──────────────────────┘ └───────────────────────┘
405  
406  end nnreal
407  
408  namespace ennreal
409  open filter
410  
411  lemma measurable_coe : measurable (coe : nnreal → ennreal) :=
id                          └────────┘  └─┘   └────┘   └─────┘
src                         └────────┘  └─┘   └────┘   └─────┘
typ                         └────────┘  └─┘   └────┘   └─────┘
doc                         └────────┘        └────┘   └─────┘
412  measurable_of_continuous (continuous_coe.2 continuous_id)
id   └──────────────────────┘  └────────────┘  └───────────┘
src  └──────────────────────┘  └────────────┘  └───────────┘
typ  └──────────────────────┘  └────────────┘  └───────────┘
413  
414  def ennreal_equiv_nnreal : measurable_equiv {r : ennreal | r < ⊤} nnreal :=
id                              └──────────────┘     └─────┘       └────┘
src                             └──────────────┘     └─────┘        └────┘
typ                             └──────────────┘     └─────┘       └────┘
doc                             └──────────────┘      └─────┘          └────┘
415  { to_fun    := λr, ennreal.to_nnreal r.1,
id                     └───────────────┘ 
src                     └───────────────┘  
typ                    └───────────────┘ 
doc                     └───────────────┘
416    inv_fun   := λr, ⟨r, coe_lt_top⟩,
id                        └────────┘
src                         └────────┘
typ                       └────────┘
417    left_inv  := assume ⟨r, hr⟩, by simp [coe_to_nnreal (ne_of_lt hr)],
id                                          └───────────┘  └──────┘ └┘
src                                    └────┘└───────────┘ └──────┘  └┘
typ                                   └────┘└───────────┘ └──────┘└┘└┘
doc                                    └────┘                        └┘
txt                                    └────┘                        └┘
par                                    └────┘                        └┘
pid                                                                └┘
st                                    └─────────────────────────────────┘
418    right_inv := assume r, to_nnreal_coe,
id                           └───────────┘
src                           └───────────┘
typ                          └───────────┘
419    measurable_to_fun  :=
420    begin
st     └─────
421      rw [← borel_eq_subtype],
id             └──────────────┘
src      └────┘└──────────────┘
typ      └────┘└──────────────┘
doc      └────┘                
txt      └────┘                
par      └────┘                
pid        └──┘                
st   ─────────────────────────┘└──
422      refine measurable_of_continuous (continuous_iff_continuous_at.2 _),
id              └──────────────────────┘  └──────────────────────────┘
src      └─────┘└──────────────────────┘ └──────────────────────────┘└───┘
typ      └─────┘└──────────────────────┘ └──────────────────────────┘└───┘
doc      └─────┘                                                     └───┘
txt      └─────┘                                                     └───┘
par      └─────┘                                                     └───┘
pid                                                                 └───┘
st   ─────────────────────────────────────────────────────────────────────┘└─
423      rintros ⟨r, hr⟩,
src      └─────────────┘
typ      └─────────────┘
doc      └─────────────┘
txt      └─────────────┘
par      └─────────────┘
pid             └──────┘
st   ──────────────────┘└─
424      simp [continuous_at, nhds_subtype_eq_comap],
id             └───────────┘  └───────────────────┘
src      └────┘└───────────┘└┘└───────────────────┘
typ      └────┘└───────────┘└┘└───────────────────┘
doc      └────┘└───────────┘└┘                     
txt      └────┘             └┘                     
par      └────┘             └┘                     
pid                       └┘                     
st   ──────────────────────────────────────────────┘└─
425      refine tendsto.comp (tendsto_to_nnreal (ne_of_lt hr)) tendsto_comap
id              └──────────┘  └───────────────┘  └──────┘ └┘   └───────────┘
src      └─────┘└──────────┘ └───────────────┘ └──────┘  └─┘└───────────┘
typ      └─────┘└──────────┘ └───────────────┘ └──────┘└┘└─┘└───────────┘
doc      └─────┘                                         └─┘             
txt      └─────┘                                         └─┘             
par      └─────┘                                         └─┘             
pid                                                     └─┘             
st   ────────────────────────────────────────────────────────────────────────
426    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
427    measurable_inv_fun := measurable.subtype_mk measurable_coe }
id                           └───────────────────┘ └────────────┘
src                          └───────────────────┘ └────────────┘
typ                          └───────────────────┘ └────────────┘
428  
429  lemma measurable_of_measurable_nnreal [measurable_space α] {f : ennreal → α}
id                                          └──────────────┘        └─────┘   
src                                         └──────────────┘         └─────┘
typ                                         └──────────────┘        └─────┘   
doc                                                                  └─────┘
430    (h : measurable (λp:nnreal, f p)) : measurable f :=
id          └────────┘     └────┘        └────────┘ 
src         └────────┘     └────┘          └────────┘
typ         └────────┘     └────┘        └────────┘ 
doc         └────────┘     └────┘          └────────┘
431  begin
st   └─────
432    refine measurable_of_measurable_union_cover {⊤} {r : ennreal | r < ⊤}
id            └──────────────────────────────────┘       └─────┘     
src    └─────┘└──────────────────────────────────┘└┘└──┘└─────┘└─┘  └─
typ    └─────┘└──────────────────────────────────┘└┘└──┘└─────┘└─┘  └─
doc    └─────┘                                      └┘ └──┘└─────┘└─┘   └─
txt    └─────┘                                      └┘ └──┘       └─┘   └─
par    └─────┘                                      └┘ └──┘       └─┘   └─
pid                                                └┘ └──┘       └─┘   └─
st   ────────────────────────────────────────────────────────────────────────
433      (is_measurable_of_is_closed $ is_closed_singleton)
id        └────────────────────────┘   └─────────────────┘
src  ───┘ └────────────────────────┘ └─────────────────┘└─
typ  ───┘ └────────────────────────┘ └─────────────────┘└─
doc  ───┘                                               └─
txt  ───┘                                               └─
par  ───┘                                               └─
pid  ───┘                                               └─
st   ───────────────────────────────────────────────────────
434      (is_measurable_of_is_open $ is_open_gt' _)
id        └──────────────────────┘   └─────────┘
src  ───┘ └──────────────────────┘ └─────────┘└───
typ  ───┘ └──────────────────────┘ └─────────┘└───
doc  ───┘                                     └───
txt  ───┘                                     └───
par  ───┘                                     └───
pid  ───┘                                     └───
st   ───────────────────────────────────────────────
435      (assume r _, by cases r; simp [ennreal.none_eq_top, ennreal.some_eq_coe])
id                                     └─────────────────┘  └─────────────────┘
src  ───┘       └────┘  └────┘ └┘└────┘└─────────────────┘└┘└─────────────────┘└─
typ  ───┘       └────┘  └────┘└┘└────┘└─────────────────┘└┘└─────────────────┘└─
doc  ───┘       └────┘  └────┘ └┘└────┘                   └┘                   └─
txt  ───┘       └────┘  └────┘ └┘└────┘                   └┘                   └─
par  ───┘       └────┘  └────┘ └┘└────┘                   └┘                   └─
pid  ───┘       └────┘  └─────┘ └──────┘                   └┘                   └──
st   ──────────────────┘└───────────────────────────────────────────────────────┘└─
436      _
src  ──────
typ  ──────
doc  ──────
txt  ──────
par  ──────
pid  ──────
st   ──────
437      _,
src  ────┘
typ  ────┘
doc  ────┘
txt  ────┘
par  ────┘
pid  ────┘
st   ────┘└─
438    exact (measurable_equiv.set.singleton ⊤).symm.measurable_coe_iff.1 (measurable_unit _),
id            └────────────────────────────┘                               └─────────────┘
src    └────┘ └────────────────────────────┘ └──────────────────────────┘ └─────────────┘└─┘
typ    └────┘ └────────────────────────────┘ └──────────────────────────┘ └─────────────┘└─┘
doc    └────┘                                └──────────────────────────┘                └─┘
txt    └────┘                                └──────────────────────────┘                └─┘
par    └────┘                                └──────────────────────────┘                └─┘
pid                                         └──────────────────────────┘                └─┘
st   ───────────────────────────────────────────────────────────────────────────────────────┘└─
439    exact (ennreal_equiv_nnreal.symm.measurable_coe_iff.1 h)
id            └──────────────────────────────────────────┘   
src    └────┘ └──────────────────────────────────────────┘└─┘ └┘
typ    └────┘ └──────────────────────────────────────────┘└─┘└┘
doc    └────┘                                             └─┘ └┘
txt    └────┘                                             └─┘ └┘
par    └────┘                                             └─┘ └┘
pid                                                      └─┘ 
st   ──────────────────────────────────────────────────────────┘
440  end
st   └─┘
441  
442  def ennreal_equiv_sum :
443    @measurable_equiv ennreal (nnreal ⊕ unit) _ sum.measurable_space :=
id      └──────────────┘ └─────┘  └────┘  └──┘    └──────────────────┘
src     └──────────────┘ └─────┘  └────┘  └──┘    └──────────────────┘
typ     └──────────────┘ └─────┘  └────┘  └──┘    └──────────────────┘
doc     └──────────────┘ └─────┘  └────┘   └──┘
444  { to_fun    :=
445      @option.rec nnreal (λ_, nnreal ⊕ unit) (sum.inr ()) (sum.inl : nnreal → nnreal ⊕ unit),
id        └────────┘ └────┘     └────┘  └──┘   └─────┘ └┘   └─────┘   └────┘   └────┘  └──┘
src       └────────┘ └────┘      └────┘  └──┘   └─────┘ └┘   └─────┘   └────┘   └────┘  └──┘
typ       └────────┘ └────┘     └────┘  └──┘   └─────┘ └┘   └─────┘   └────┘   └────┘  └──┘
doc                  └────┘      └────┘   └──┘                          └────┘   └────┘   └──┘
446    inv_fun   :=
447      @sum.rec nnreal unit (λ_, ennreal) (coe : nnreal → ennreal) (λ_, ⊤),
id        └─────┘ └────┘ └──┘     └─────┘   └─┘   └────┘   └─────┘      
src       └─────┘ └────┘ └──┘      └─────┘   └─┘   └────┘   └─────┘       
typ       └─────┘ └────┘ └──┘     └─────┘   └─┘   └────┘   └─────┘      
doc               └────┘ └──┘      └─────┘         └────┘   └─────┘
448    left_inv  := assume s, by cases s; refl,
id                                    
src                              └────┘   └──┘
typ                             └────┘  └──┘
doc                              └────┘   └──┘
txt                              └────┘   └──┘
par                              └────┘   └──┘
pid                                   
st                              └────────────┘
449    right_inv := assume s, by rcases s with r | ⟨⟨⟩⟩; refl,
id                                     
src                              └─────┘ └────────────┘  └──┘
typ                             └─────┘└────────────┘  └──┘
doc                              └─────┘ └────────────┘  └──┘
txt                              └─────┘ └────────────┘  └──┘
par                              └─────┘ └────────────┘  └──┘
pid                                     └────────────┘
st                              └───────────────────────────┘
450    measurable_to_fun  := measurable_of_measurable_nnreal measurable_inl,
id                           └─────────────────────────────┘ └────────────┘
src                          └─────────────────────────────┘ └────────────┘
typ                          └─────────────────────────────┘ └────────────┘
451    measurable_inv_fun := measurable_sum measurable_coe (@measurable_const ennreal unit _ _ ⊤) }
id                           └────────────┘ └────────────┘   └──────────────┘ └─────┘ └──┘     
src                          └────────────┘ └────────────┘   └──────────────┘ └─────┘ └──┘     
typ                          └────────────┘ └────────────┘   └──────────────┘ └─────┘ └──┘     
doc                                                                           └─────┘ └──┘
452  
453  lemma measurable_of_measurable_nnreal_nnreal [measurable_space α] [measurable_space β]
id                                                 └──────────────┘    └──────────────┘ 
src                                                └──────────────┘     └──────────────┘
typ                                                └──────────────┘    └──────────────┘ 
454    (f : ennreal → ennreal → β) {g : α → ennreal} {h : α → ennreal}
id          └─────┘   └─────┘             └─────┘          └─────┘
src         └─────┘   └─────┘               └─────┘           └─────┘
typ         └─────┘   └─────┘             └─────┘          └─────┘
doc         └─────┘   └─────┘               └─────┘           └─────┘
455    (h₁ : measurable (λp:nnreal × nnreal, f p.1 p.2))
id           └────────┘     └────┘  └────┘     
src          └────────┘     └────┘  └────┘        
typ          └────────┘     └────┘  └────┘     
doc          └────────┘     └────┘   └────┘
456    (h₂ : measurable (λr:nnreal, f ⊤ r))
id           └────────┘     └────┘    
src          └────────┘     └────┘    
typ          └────────┘     └────┘    
doc          └────────┘     └────┘
457    (h₃ : measurable (λr:nnreal, f r ⊤))
id           └────────┘     └────┘    
src          └────────┘     └────┘      
typ          └────────┘     └────┘    
doc          └────────┘     └────┘
458    (hg : measurable g) (hh : measurable h) : measurable (λa, f (g a) (h a)) :=
id           └────────┘         └────────┘     └────────┘            
src          └────────┘          └────────┘      └────────┘
typ          └────────┘         └────────┘     └────────┘            
doc          └────────┘          └────────┘      └────────┘
459  let e : measurable_equiv (ennreal × ennreal)
id           └──────────────┘  └─────┘  └─────┘
src          └──────────────┘  └─────┘  └─────┘
typ          └──────────────┘  └─────┘  └─────┘
doc          └──────────────┘  └─────┘   └─────┘
460    (((nnreal × nnreal) ⊕ (nnreal × unit)) ⊕ ((unit × nnreal) ⊕ (unit × unit))) :=
id        └────┘  └────┘    └────┘  └──┘      └──┘  └────┘    └──┘  └──┘
src       └────┘  └────┘    └────┘  └──┘      └──┘  └────┘    └──┘  └──┘
typ       └────┘  └────┘    └────┘  └──┘      └──┘  └────┘    └──┘  └──┘
doc       └────┘   └────┘     └────┘   └──┘       └──┘   └────┘     └──┘   └──┘
461    (measurable_equiv.prod_congr ennreal_equiv_sum ennreal_equiv_sum).trans
id      └─────────────────────────┘ └───────────────┘ └───────────────┘ └───┘
src     └─────────────────────────┘ └───────────────┘ └───────────────┘ └───┘
typ     └─────────────────────────┘ └───────────────┘ └───────────────┘ └───┘
462      (measurable_equiv.sum_prod_sum _ _ _ _) in
id        └───────────────────────────┘
src       └───────────────────────────┘
typ       └───────────────────────────┘
463  have measurable (λp:ennreal×ennreal, f p.1 p.2),
id        └────────┘     └─────┘└─────┘     
src       └────────┘     └─────┘└─────┘        
typ       └────────┘     └─────┘└─────┘     
doc       └────────┘     └─────┘ └─────┘
464  begin
st   └─────
465    refine e.symm.measurable_coe_iff.1 (measurable_sum (measurable_sum _ _) (measurable_sum _ _)),
id            └───────────────────────┘                                         └────────────┘
src    └─────┘└───────────────────────┘└─┘                              └────┘ └────────────┘└────┘
typ    └─────┘└───────────────────────┘└─┘                              └────┘ └────────────┘└────┘
doc    └─────┘                         └─┘                              └────┘               └────┘
txt    └─────┘                         └─┘                              └────┘               └────┘
par    └─────┘                         └─┘                              └────┘               └────┘
pid                                   └─┘                              └────┘               └────┘
st   ──────────────────────────────────────────────────────────────────────────────────────────────┘└─
466    { show measurable (λp:nnreal × nnreal, f p.1 p.2),
id            └────────┘             └────┘  
src      └───┘└────────┘  └┘      └────┘└┘  └─┘ └─┘
typ      └───┘└────────┘  └┘      └────┘└┘ └─┘ └─┘
doc      └───┘└────────┘  └┘       └────┘└┘  └─┘ └─┘
txt      └───┘            └┘             └┘  └─┘ └─┘
par      └───┘            └┘             └┘  └─┘ └─┘
pid      └───┘            └┘             └┘  └─┘ └─┘
st   ───┘└─────────────────────────────────────────────┘└─
467      exact h₁ },
id             └┘
src      └────┘  
typ      └────┘└┘
doc      └────┘  
txt      └────┘  
par      └────┘  
pid             
st   ────────────┘└┘
468    { show measurable (λp:nnreal × unit, f p.1 ⊤),
id            └────────┘     └────┘  └──┘       
src      └───┘└────────┘  └┘└────┘ └──┘└┘  └─┘
typ      └───┘└────────┘  └┘└────┘└──┘└┘ └─┘
doc      └───┘└────────┘  └┘└────┘ └──┘└┘  └─┘ 
txt      └───┘            └┘           └┘  └─┘ 
par      └───┘            └┘           └┘  └─┘ 
pid      └───┘            └┘           └┘  └─┘ 
st   ───┘└─────────────────────────────────────────┘└─
469      exact h₃.comp (measurable.fst measurable_id) },
id             └─────┘  └────────────┘ └───────────┘
src      └────┘└─────┘ └────────────┘└───────────┘└┘
typ      └────┘└─────┘ └────────────┘└───────────┘└┘
doc      └────┘                                   └┘
txt      └────┘                                   └┘
par      └────┘                                   └┘
pid                                              
st   ────────────────────────────────────────────────┘└┘
470    { show measurable ((λp:nnreal, f ⊤ p) ∘ (λp:unit × nnreal, p.2)),
id            └────────┘                         └──┘  └────┘
src      └───┘└────────┘   └┘      └┘   └┘  └┘└──┘ └────┘└┘ └──┘
typ      └───┘└────────┘   └┘      └┘  └┘  └┘└──┘└────┘└┘ └──┘
doc      └───┘└────────┘   └┘      └┘   └┘   └┘└──┘ └────┘└┘ └──┘
txt      └───┘             └┘      └┘   └┘   └┘           └┘ └──┘
par      └───┘             └┘      └┘   └┘   └┘           └┘ └──┘
pid      └───┘             └┘      └┘   └┘   └┘           └┘ └──┘
st   ───┘└────────────────────────────────────────────────────────────┘└─
471      exact h₂.comp (measurable.snd measurable_id) },
id             └─────┘  └────────────┘ └───────────┘
src      └────┘└─────┘ └────────────┘└───────────┘└┘
typ      └────┘└─────┘ └────────────┘└───────────┘└┘
doc      └────┘                                   └┘
txt      └────┘                                   └┘
par      └────┘                                   └┘
pid                                              
st   ────────────────────────────────────────────────┘└┘
472    { show measurable (λp:unit × unit, f ⊤ ⊤),
id            └────────┘           └──┘  
src      └───┘└────────┘  └┘     └──┘└┘   
typ      └───┘└────────┘  └┘    └──┘└┘  
doc      └───┘└────────┘  └┘     └──┘└┘   
txt      └───┘            └┘         └┘   
par      └───┘            └┘         └┘   
pid      └───┘            └┘         └┘   
st   ──────────────────────────────────────────┘└─
473      exact measurable_const }
id             └──────────────┘
src      └────┘└──────────────┘
typ      └────┘└──────────────┘
doc      └────┘                
txt      └────┘                
par      └────┘                
pid                           
st   ──────────────────────────┘└─
474  end,
st   ──┘
475  this.comp (measurable.prod_mk hg hh)
id   └──┘└───┘  └────────────────┘ └┘ └┘
src      └───┘  └────────────────┘
typ  └──┘└───┘  └────────────────┘ └┘ └┘
476  
477  lemma measurable.mul {α : Type*} [measurable_space α] {f g : α → ennreal} :
id                                     └──────────────┘             └─────┘
src                                    └──────────────┘               └─────┘
typ                                    └──────────────┘             └─────┘
doc                                                                   └─────┘
478    measurable f → measurable g → measurable (λa, f a * g a) :=
id     └────────┘    └────────┘    └────────┘         
src    └────────┘     └────────┘     └────────┘          
typ    └────────┘    └────────┘    └────────┘         
doc    └────────┘     └────────┘     └────────┘
479  begin
st   └─────
480    refine measurable_of_measurable_nnreal_nnreal (*) _ _ _,
id            └────────────────────────────────────┘ 
src    └─────┘└────────────────────────────────────┘└──────┘
typ    └─────┘└────────────────────────────────────┘└──────┘
doc    └─────┘                                       └──────┘
txt    └─────┘                                       └──────┘
par    └─────┘                                       └──────┘
pid                                                 └──────┘
st   ────────────────────────────────────────────────────────┘└─
481    { simp only [ennreal.coe_mul.symm],
src      └─────────┘                    
typ      └─────────┘└──────────────────┘
doc      └─────────┘                    
txt      └─────────┘                    
par      └─────────┘                    
pid          └──┘└┘                    
st   ───┘└──────────────────────────────┘└─
482      exact measurable_coe.comp
id             └─────────────────┘
src      └────┘└─────────────────┘
typ      └────┘└─────────────────┘
doc      └────┘                   
txt      └────┘                   
par      └────┘                   
pid                              
st   ──────────────────────────────
483        (measurable.mul (measurable.fst measurable_id) (measurable.snd measurable_id)) },
id          └────────────┘  └────────────┘                 └────────────┘ └───────────┘
src  ─────┘ └────────────┘ └────────────┘             └┘ └────────────┘└───────────┘└─┘
typ  ─────┘ └────────────┘ └────────────┘             └┘ └────────────┘└───────────┘└─┘
doc  ─────┘                                           └┘                            └─┘
txt  ─────┘                                           └┘                            └─┘
par  ─────┘                                           └┘                            └─┘
pid  ─────┘                                           └┘                            └┘
st   ────────────────────────────────────────────────────────────────────────────────────┘└┘
484    { simp [top_mul],
id             └─────┘
src      └────┘└─────┘
typ      └────┘└─────┘
doc      └────┘       
txt      └────┘       
par      └────┘       
pid                 
st   ───┘└────────────┘└─
485      exact measurable.if
id             └───────────┘
src      └────┘└───────────┘
typ      └────┘└───────────┘
doc      └────┘             
txt      └────┘             
par      └────┘             
pid                        
st   ────────────────────────
486        (is_measurable_of_is_closed $ is_closed_eq continuous_id continuous_const)
id          └────────────────────────┘   └──────────┘ └───────────┘ └──────────────┘
src  ─────┘ └────────────────────────┘ └──────────┘└───────────┘└──────────────┘└─
typ  ─────┘ └────────────────────────┘ └──────────┘└───────────┘└──────────────┘└─
doc  ─────┘                                                                     └─
txt  ─────┘                                                                     └─
par  ─────┘                                                                     └─
pid  ─────┘                                                                     └─
st   ─────────────────────────────────────────────────────────────────────────────────
487        measurable_const
src  ─────┘                
typ  ─────┘                
doc  ─────┘                
txt  ─────┘                
par  ─────┘                
pid  ─────┘                
st   ───────────────────────
488        measurable_const },
id         └──────────────┘
src  ─────┘└──────────────┘
typ  ─────┘└──────────────┘
doc  ─────┘                
txt  ─────┘                
par  ─────┘                
pid  ─────┘                
st   ──────────────────────┘└┘
489    { simp [mul_top],
id             └─────┘
src      └────┘└─────┘
typ      └────┘└─────┘
doc      └────┘       
txt      └────┘       
par      └────┘       
pid                 
st   ─────────────────┘└─
490      exact measurable.if
id             └───────────┘
src      └────┘└───────────┘
typ      └────┘└───────────┘
doc      └────┘             
txt      └────┘             
par      └────┘             
pid                        
st   ────────────────────────
491        (is_measurable_of_is_closed $ is_closed_eq continuous_id continuous_const)
id          └────────────────────────┘   └──────────┘ └───────────┘ └──────────────┘
src  ─────┘ └────────────────────────┘ └──────────┘└───────────┘└──────────────┘└─
typ  ─────┘ └────────────────────────┘ └──────────┘└───────────┘└──────────────┘└─
doc  ─────┘                                                                     └─
txt  ─────┘                                                                     └─
par  ─────┘                                                                     └─
pid  ─────┘                                                                     └─
st   ─────────────────────────────────────────────────────────────────────────────────
492        measurable_const
src  ─────┘                
typ  ─────┘                
doc  ─────┘                
txt  ─────┘                
par  ─────┘                
pid  ─────┘                
st   ───────────────────────
493        measurable_const }
id         └──────────────┘
src  ─────┘└──────────────┘
typ  ─────┘└──────────────┘
doc  ─────┘                
txt  ─────┘                
par  ─────┘                
pid  ─────┘                
st   ──────────────────────┘└─
494  end
st   ──┘
495  
496  lemma measurable.add {α : Type*} [measurable_space α] {f g : α → ennreal} :
id                                     └──────────────┘             └─────┘
src                                    └──────────────┘               └─────┘
typ                                    └──────────────┘             └─────┘
doc                                                                   └─────┘
497    measurable f → measurable g → measurable (λa, f a + g a) :=
id     └────────┘    └────────┘    └────────┘         
src    └────────┘     └────────┘     └────────┘          
typ    └────────┘    └────────┘    └────────┘         
doc    └────────┘     └────────┘     └────────┘
498  begin
st   └─────
499    refine measurable_of_measurable_nnreal_nnreal (+) _ _ _,
id            └────────────────────────────────────┘ 
src    └─────┘└────────────────────────────────────┘└──────┘
typ    └─────┘└────────────────────────────────────┘└──────┘
doc    └─────┘                                       └──────┘
txt    └─────┘                                       └──────┘
par    └─────┘                                       └──────┘
pid                                                 └──────┘
st   ────────────────────────────────────────────────────────┘└─
500    { simp only [ennreal.coe_add.symm],
src      └─────────┘                    
typ      └─────────┘└──────────────────┘
doc      └─────────┘                    
txt      └─────────┘                    
par      └─────────┘                    
pid          └──┘└┘                    
st   ───┘└──────────────────────────────┘└─
501      exact measurable_coe.comp
id             └─────────────────┘
src      └────┘└─────────────────┘
typ      └────┘└─────────────────┘
doc      └────┘                   
txt      └────┘                   
par      └────┘                   
pid                              
st   ──────────────────────────────
502        (measurable.add (measurable.fst measurable_id) (measurable.snd measurable_id)) },
id          └────────────┘  └────────────┘                 └────────────┘ └───────────┘
src  ─────┘ └────────────┘ └────────────┘             └┘ └────────────┘└───────────┘└─┘
typ  ─────┘ └────────────┘ └────────────┘             └┘ └────────────┘└───────────┘└─┘
doc  ─────┘                                           └┘                            └─┘
txt  ─────┘                                           └┘                            └─┘
par  ─────┘                                           └┘                            └─┘
pid  ─────┘                                           └┘                            └┘
st   ────────────────────────────────────────────────────────────────────────────────────┘└┘
503    { simp [measurable_const] },
id             └──────────────┘
src      └────┘└──────────────┘└┘
typ      └────┘└──────────────┘└┘
doc      └────┘                └┘
txt      └────┘                └┘
par      └────┘                └┘
pid                          
st   ───┘└──────────────────────┘└┘
504    { simp [measurable_const] }
id             └──────────────┘
src      └────┘└──────────────┘└┘
typ      └────┘└──────────────┘└┘
doc      └────┘                └┘
txt      └────┘                └┘
par      └────┘                └┘
pid                          
st   ───────────────────────────┘└─
505  end
st   ──┘
506  
507  lemma measurable.sub {α : Type*} [measurable_space α] {f g : α → ennreal} :
id                                     └──────────────┘             └─────┘
src                                    └──────────────┘               └─────┘
typ                                    └──────────────┘             └─────┘
doc                                                                   └─────┘
508    measurable f → measurable g → measurable (λa, f a - g a) :=
id     └────────┘    └────────┘    └────────┘         
src    └────────┘     └────────┘     └────────┘          
typ    └────────┘    └────────┘    └────────┘         
doc    └────────┘     └────────┘     └────────┘
509  begin
st   └─────
510    refine measurable_of_measurable_nnreal_nnreal (has_sub.sub) _ _ _,
id            └────────────────────────────────────┘  └─────────┘
src    └─────┘└────────────────────────────────────┘ └─────────┘└─────┘
typ    └─────┘└────────────────────────────────────┘ └─────────┘└─────┘
doc    └─────┘                                                  └─────┘
txt    └─────┘                                                  └─────┘
par    └─────┘                                                  └─────┘
pid                                                            └─────┘
st   ──────────────────────────────────────────────────────────────────┘└─
511    { simp only [ennreal.coe_sub.symm],
src      └─────────┘                    
typ      └─────────┘└──────────────────┘
doc      └─────────┘                    
txt      └─────────┘                    
par      └─────────┘                    
pid          └──┘└┘                    
st   ───┘└──────────────────────────────┘└─
512      exact measurable_coe.comp
id             └─────────────────┘
src      └────┘└─────────────────┘
typ      └────┘└─────────────────┘
doc      └────┘                   
txt      └────┘                   
par      └────┘                   
pid                              
st   ──────────────────────────────
513        (nnreal.measurable.sub (measurable.fst measurable_id) (measurable.snd measurable_id)) },
id          └───────────────────┘  └────────────┘                 └────────────┘ └───────────┘
src  ─────┘ └───────────────────┘ └────────────┘             └┘ └────────────┘└───────────┘└─┘
typ  ─────┘ └───────────────────┘ └────────────┘             └┘ └────────────┘└───────────┘└─┘
doc  ─────┘                                                  └┘                            └─┘
txt  ─────┘                                                  └┘                            └─┘
par  ─────┘                                                  └┘                            └─┘
pid  ─────┘                                                  └┘                            └┘
st   ───────────────────────────────────────────────────────────────────────────────────────────┘└┘
514    { simp [measurable_const] },
id             └──────────────┘
src      └────┘└──────────────┘└┘
typ      └────┘└──────────────┘└┘
doc      └────┘                └┘
txt      └────┘                └┘
par      └────┘                └┘
pid                          
st   ───┘└──────────────────────┘└┘
515    { simp [measurable_const] }
id             └──────────────┘
src      └────┘└──────────────┘└┘
typ      └────┘└──────────────┘└┘
doc      └────┘                └┘
txt      └────┘                └┘
par      └────┘                └┘
pid                          
st   ───────────────────────────┘└─
516  end
st   ──┘
517  
518  lemma measurable_of_real : measurable ennreal.of_real :=
id                              └────────┘ └─────────────┘
src                             └────────┘ └─────────────┘
typ                             └────────┘ └─────────────┘
doc                             └────────┘ └─────────────┘
519  measurable_of_continuous ennreal.continuous_of_real
id   └──────────────────────┘ └────────────────────────┘
src  └──────────────────────┘ └────────────────────────┘
typ  └──────────────────────┘ └────────────────────────┘
520  
521  end ennreal
522  
523  open topological_space
524  
525  lemma measurable.smul' {α : Type*} {β : Type*} {γ : Type*}
526    [semiring α] [topological_space α] [second_countable_topology α]
id      └──────┘    └───────────────┘    └───────────────────────┘ 
src     └──────┘     └───────────────┘     └───────────────────────┘
typ     └──────┘    └───────────────┘    └───────────────────────┘ 
doc                  └───────────────┘     └───────────────────────┘
527    [topological_space β] [add_comm_monoid β] [second_countable_topology β]
id      └───────────────┘    └─────────────┘    └───────────────────────┘ 
src     └───────────────┘     └─────────────┘     └───────────────────────┘
typ     └───────────────┘    └─────────────┘    └───────────────────────┘ 
doc     └───────────────┘                         └───────────────────────┘
528    [semimodule α β] [topological_semimodule α β] [measurable_space γ]
id      └────────┘     └────────────────────┘     └──────────────┘ 
src     └────────┘       └────────────────────┘       └──────────────┘
typ     └────────┘     └────────────────────┘     └──────────────┘ 
doc     └────────┘       └────────────────────┘
529    {f : γ → α} {g : γ → β} (hf : measurable f) (hg : measurable g) :
id                               └────────┘         └────────┘ 
src                                  └────────┘          └────────┘
typ                              └────────┘         └────────┘ 
doc                                  └────────┘          └────────┘
530    measurable (λ c, f c • g c) :=
id     └────────┘          
src    └────────┘           
typ    └────────┘          
doc    └────────┘
531  measurable_of_continuous2 (continuous_fst.smul continuous_snd) hf hg
id   └───────────────────────┘  └────────────┘└───┘ └────────────┘  └┘ └┘
src  └───────────────────────┘  └────────────┘└───┘ └────────────┘
typ  └───────────────────────┘  └────────────┘└───┘ └────────────┘  └┘ └┘
532  
533  lemma measurable.smul {α : Type*} {β : Type*} {γ : Type*}
534    [semiring α] [topological_space α]
id      └──────┘    └───────────────┘ 
src     └──────┘     └───────────────┘
typ     └──────┘    └───────────────┘ 
doc                  └───────────────┘
535    [topological_space β] [add_comm_monoid β]
id      └───────────────┘    └─────────────┘ 
src     └───────────────┘     └─────────────┘
typ     └───────────────┘    └─────────────┘ 
doc     └───────────────┘
536    [semimodule α β] [topological_semimodule α β] [measurable_space γ]
id      └────────┘     └────────────────────┘     └──────────────┘ 
src     └────────┘       └────────────────────┘       └──────────────┘
typ     └────────┘     └────────────────────┘     └──────────────┘ 
doc     └────────┘       └────────────────────┘
537    (c : α) {f : γ → β} (hf : measurable f) : measurable (λ x, c • f x) :=
id                            └────────┘     └────────┘         
src                              └────────┘      └────────┘         
typ                           └────────┘     └────────┘         
doc                              └────────┘      └────────┘
538  measurable.comp (measurable_of_continuous (continuous_const.smul continuous_id)) hf
id   └─────────────┘  └──────────────────────┘  └──────────────┘└───┘ └───────────┘   └┘
src  └─────────────┘  └──────────────────────┘  └──────────────┘└───┘ └───────────┘
typ  └─────────────┘  └──────────────────────┘  └──────────────┘└───┘ └───────────┘   └┘
539  
540  lemma measurable_smul_iff {α : Type*} {β : Type*} {γ : Type*}
541    [division_ring α] [topological_space α]
id      └───────────┘    └───────────────┘ 
src     └───────────┘     └───────────────┘
typ     └───────────┘    └───────────────┘ 
doc                       └───────────────┘
542    [topological_space β] [add_comm_monoid β]
id      └───────────────┘    └─────────────┘ 
src     └───────────────┘     └─────────────┘
typ     └───────────────┘    └─────────────┘ 
doc     └───────────────┘
543    [semimodule α β] [topological_semimodule α β] [measurable_space γ]
id      └────────┘     └────────────────────┘     └──────────────┘ 
src     └────────┘       └────────────────────┘       └──────────────┘
typ     └────────┘     └────────────────────┘     └──────────────┘ 
doc     └────────┘       └────────────────────┘
544    {c : α} (hc : c ≠ 0) (f : γ → β) : measurable (λ x, c • f x) ↔ measurable f :=
id                                   └────────┘            └────────┘ 
src                                      └────────┘                └────────┘
typ                                  └────────┘            └────────┘ 
doc                                       └────────┘                  └────────┘
545  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
546  begin
st   └─────
547    assume h,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid    └──────┘
st   ─────────┘└─
548    have eq : (λ (x : γ), c⁻¹ • (λ (x : γ), c • f x) x) = f,
id                            └┘                         
src    └────────┘  └────┘ └─┘ └┘  └────┘ └─┘    └┘ └┘
typ    └────────┘  └────┘ └─┘ └┘  └────┘└─┘   └┘ └┘
doc    └────────┘  └────┘ └─┘      └────┘ └─┘    └┘ └┘ 
txt    └────────┘  └────┘ └─┘      └────┘ └─┘    └┘ └┘ 
par    └────────┘  └────┘ └─┘      └────┘ └─┘    └┘ └┘ 
pid    └─────┘└─┘  └────┘ └─┘      └────┘ └─┘    └┘ └┘ 
st   ────────────────────────────────────────────────────────┘└─
549    { funext, rw [smul_smul, inv_mul_cancel hc, one_smul] },
id                   └───────┘  └────────────┘ └┘  └──────┘
src      └────┘  └──┘└───────┘└┘└────────────┘  └┘└──────┘└┘
typ      └────┘  └──┘└───────┘└┘└────────────┘└┘└┘└──────┘└┘
doc      └────┘  └──┘         └┘                └┘        └┘
txt      └────┘  └──┘         └┘                └┘        └┘
par      └────┘  └──┘         └┘                └┘        └┘
pid                └┘         └┘                └┘        
st   ───┘└────┘└─────────────┘└─────────────────┘└────────┘└┘
550    have := h.smul c⁻¹,
id             └────┘ 
src    └──────┘└────┘
typ    └──────┘└────┘
doc    └──────┘      
txt    └──────┘      
par    └──────┘      
pid    └───┘└─┘      
st   ───────────────────┘└─
551    rwa eq at this
id         └┘
src    └──┘└┘└───────┘
typ    └──┘└┘└───────┘
doc    └──┘  └───────┘
txt    └──┘  └───────┘
par    └──┘  └───────┘
pid         └──────┘
st   ────────────────┘
552  end
st   └─┘
553  $ measurable.smul c
id     └─────────────┘ 
src    └─────────────┘
typ    └─────────────┘ 
554  
555  lemma measurable_dist {α : Type*} [metric_space α] [second_countable_topology α] :
id                                      └──────────┘    └───────────────────────┘ 
src                                     └──────────┘     └───────────────────────┘
typ                                     └──────────┘    └───────────────────────┘ 
doc                                     └──────────┘     └───────────────────────┘
556    measurable (λp:α×α, dist p.1 p.2) :=
id     └────────┘       └──┘   
src    └────────┘         └──┘     
typ    └────────┘       └──┘   
doc    └────────┘
557  begin
st   └─────
558    rw [borel_prod],
id         └────────┘
src    └──┘└────────┘
typ    └──┘└────────┘
doc    └──┘          
txt    └──┘          
par    └──┘          
pid      └┘          
st   ───────────────┘└──
559    apply measurable_of_continuous,
id           └──────────────────────┘
src    └────┘└──────────────────────┘
typ    └────┘└──────────────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ───────────────────────────────┘└─
560    exact continuous_dist continuous_fst continuous_snd
id           └─────────────┘ └────────────┘ └────────────┘
src    └────┘└─────────────┘└────────────┘└────────────┘
typ    └────┘└─────────────┘└────────────┘└────────────┘
doc    └────┘                                           
txt    └────┘                                           
par    └────┘                                           
pid                                                    
st   ─────────────────────────────────────────────────────┘
561  end
st   └─┘
562  
563  lemma measurable.dist {α : Type*} [metric_space α] [second_countable_topology α]
id                                      └──────────┘    └───────────────────────┘ 
src                                     └──────────┘     └───────────────────────┘
typ                                     └──────────┘    └───────────────────────┘ 
doc                                     └──────────┘     └───────────────────────┘
564    [measurable_space β] {f g : β → α} (hf : measurable f) (hg : measurable g) :
id      └──────────────┘                     └────────┘         └────────┘ 
src     └──────────────┘                        └────────┘          └────────┘
typ     └──────────────┘                     └────────┘         └────────┘ 
doc                                             └────────┘          └────────┘
565  	measurable (λ b, dist (f b) (g b)) :=
id    └────────┘      └──┘       
src   └────────┘       └──┘
typ   └────────┘      └──┘       
doc   └────────┘
566  measurable_dist.comp (measurable.prod_mk hf hg)
id   └─────────────┘└───┘  └────────────────┘ └┘ └┘
src  └─────────────┘└───┘  └────────────────┘
typ  └─────────────┘└───┘  └────────────────┘ └┘ └┘
567  
568  lemma measurable_nndist {α : Type*} [metric_space α] [second_countable_topology α] :
id                                        └──────────┘    └───────────────────────┘ 
src                                       └──────────┘     └───────────────────────┘
typ                                       └──────────┘    └───────────────────────┘ 
doc                                       └──────────┘     └───────────────────────┘
569    measurable (λp:α×α, nndist p.1 p.2) :=
id     └────────┘       └────┘   
src    └────────┘         └────┘     
typ    └────────┘       └────┘   
doc    └────────┘          └────┘
570  begin
st   └─────
571    rw [borel_prod],
id         └────────┘
src    └──┘└────────┘
typ    └──┘└────────┘
doc    └──┘          
txt    └──┘          
par    └──┘          
pid      └┘          
st   ───────────────┘└──
572    apply measurable_of_continuous,
id           └──────────────────────┘
src    └────┘└──────────────────────┘
typ    └────┘└──────────────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ───────────────────────────────┘└─
573    exact continuous_nndist continuous_fst continuous_snd
id           └───────────────┘ └────────────┘ └────────────┘
src    └────┘└───────────────┘└────────────┘└────────────┘
typ    └────┘└───────────────┘└────────────┘└────────────┘
doc    └────┘                                             
txt    └────┘                                             
par    └────┘                                             
pid                                                      
st   ───────────────────────────────────────────────────────┘
574  end
st   └─┘
575  
576  lemma measurable.nndist {α : Type*} [metric_space α] [second_countable_topology α]
id                                        └──────────┘    └───────────────────────┘ 
src                                       └──────────┘     └───────────────────────┘
typ                                       └──────────┘    └───────────────────────┘ 
doc                                       └──────────┘     └───────────────────────┘
577    [measurable_space β] {f g : β → α} (hf : measurable f) (hg : measurable g) :
id      └──────────────┘                     └────────┘         └────────┘ 
src     └──────────────┘                        └────────┘          └────────┘
typ     └──────────────┘                     └────────┘         └────────┘ 
doc                                             └────────┘          └────────┘
578  	measurable (λ b, nndist (f b) (g b)) :=
id    └────────┘      └────┘       
src   └────────┘       └────┘
typ   └────────┘      └────┘       
doc   └────────┘       └────┘
579  measurable_nndist.comp (measurable.prod_mk hf hg)
id   └───────────────┘└───┘  └────────────────┘ └┘ └┘
src  └───────────────┘└───┘  └────────────────┘
typ  └───────────────┘└───┘  └────────────────┘ └┘ └┘
580  
581  lemma measurable_edist {α : Type*} [emetric_space α] [second_countable_topology α] :
id                                       └───────────┘    └───────────────────────┘ 
src                                      └───────────┘     └───────────────────────┘
typ                                      └───────────┘    └───────────────────────┘ 
doc                                      └───────────┘     └───────────────────────┘
582    measurable (λp:α×α, edist p.1 p.2) :=
id     └────────┘       └───┘   
src    └────────┘         └───┘     
typ    └────────┘       └───┘   
doc    └────────┘
583  begin
st   └─────
584    rw [borel_prod],
id         └────────┘
src    └──┘└────────┘
typ    └──┘└────────┘
doc    └──┘          
txt    └──┘          
par    └──┘          
pid      └┘          
st   ───────────────┘└──
585    apply measurable_of_continuous,
id           └──────────────────────┘
src    └────┘└──────────────────────┘
typ    └────┘└──────────────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ───────────────────────────────┘└─
586    exact continuous_edist continuous_fst continuous_snd
id           └──────────────┘ └────────────┘ └────────────┘
src    └────┘└──────────────┘└────────────┘└────────────┘
typ    └────┘└──────────────┘└────────────┘└────────────┘
doc    └────┘                                            
txt    └────┘                                            
par    └────┘                                            
pid                                                     
st   ──────────────────────────────────────────────────────┘
587  end
st   └─┘
588  
589  lemma measurable.edist {α : Type*} [emetric_space α] [second_countable_topology α]
id                                       └───────────┘    └───────────────────────┘ 
src                                      └───────────┘     └───────────────────────┘
typ                                      └───────────┘    └───────────────────────┘ 
doc                                      └───────────┘     └───────────────────────┘
590    [measurable_space β] {f g : β → α} (hf : measurable f) (hg : measurable g) :
id      └──────────────┘                     └────────┘         └────────┘ 
src     └──────────────┘                        └────────┘          └────────┘
typ     └──────────────┘                     └────────┘         └────────┘ 
doc                                             └────────┘          └────────┘
591  	measurable (λ b, edist (f b) (g b)) :=
id    └────────┘      └───┘       
src   └────────┘       └───┘
typ   └────────┘      └───┘       
doc   └────────┘
592  measurable_edist.comp (measurable.prod_mk hf hg)
id   └──────────────┘└───┘  └────────────────┘ └┘ └┘
src  └──────────────┘└───┘  └────────────────┘
typ  └──────────────┘└───┘  └────────────────┘ └┘ └┘
593  
594  lemma measurable_norm {α : Type*} [normed_group α] : measurable (norm : α → ℝ) :=
id                                      └──────────┘     └────────┘  └──┘      
src                                     └──────────┘      └────────┘  └──┘       
typ                                     └──────────┘     └────────┘  └──┘      
doc                                     └──────────┘      └────────┘
595  measurable_of_continuous continuous_norm
id   └──────────────────────┘ └─────────────┘
src  └──────────────────────┘ └─────────────┘
typ  └──────────────────────┘ └─────────────┘
596  
597  lemma measurable.norm {α : Type*} [normed_group α] [measurable_space β]
id                                      └──────────┘    └──────────────┘ 
src                                     └──────────┘     └──────────────┘
typ                                     └──────────┘    └──────────────┘ 
doc                                     └──────────┘
598    {f : β → α} (hf : measurable f) : measurable (λa, norm (f a)) :=
id                     └────────┘     └────────┘     └──┘   
src                      └────────┘      └────────┘      └──┘
typ                    └────────┘     └────────┘     └──┘   
doc                      └────────┘      └────────┘
599  measurable_norm.comp hf
id   └─────────────┘└───┘ └┘
src  └─────────────┘└───┘
typ  └─────────────┘└───┘ └┘
600  
601  lemma measurable_nnnorm {α : Type*} [normed_group α] : measurable (nnnorm : α → nnreal) :=
id                                        └──────────┘     └────────┘  └────┘      └────┘
src                                       └──────────┘      └────────┘  └────┘       └────┘
typ                                       └──────────┘     └────────┘  └────┘      └────┘
doc                                       └──────────┘      └────────┘  └────┘       └────┘
602  measurable_of_continuous continuous_nnnorm
id   └──────────────────────┘ └───────────────┘
src  └──────────────────────┘ └───────────────┘
typ  └──────────────────────┘ └───────────────┘
603  
604  lemma measurable.nnnorm {α : Type*} [normed_group α] [measurable_space β]
id                                        └──────────┘    └──────────────┘ 
src                                       └──────────┘     └──────────────┘
typ                                       └──────────┘    └──────────────┘ 
doc                                       └──────────┘
605    {f : β → α} (hf : measurable f) : measurable (λa, nnnorm (f a)) :=
id                     └────────┘     └────────┘     └────┘   
src                      └────────┘      └────────┘      └────┘
typ                    └────────┘     └────────┘     └────┘   
doc                      └────────┘      └────────┘      └────┘
606  measurable_nnnorm.comp hf
id   └───────────────┘└───┘ └┘
src  └───────────────┘└───┘
typ  └───────────────┘└───┘ └┘
607  
608  lemma measurable.coe_nnnorm {α : Type*} [normed_group α] [measurable_space β]
id                                            └──────────┘    └──────────────┘ 
src                                           └──────────┘     └──────────────┘
typ                                           └──────────┘    └──────────────┘ 
doc                                           └──────────┘
609    {f : β → α} (hf : measurable f) : measurable (λa, (nnnorm (f a) : ennreal)) :=
id                     └────────┘     └────────┘      └────┘       └─────┘
src                      └────────┘      └────────┘       └────┘         └─────┘
typ                    └────────┘     └────────┘      └────┘       └─────┘
doc                      └────────┘      └────────┘       └────┘         └─────┘
610  ennreal.measurable_coe.comp $ hf.nnnorm
id   └────────────────────┘└───┘   └┘└─────┘
src  └────────────────────┘└───┘     └─────┘
typ  └────────────────────┘└───┘   └┘└─────┘